(T : F →L[ℂ] F) {k l : ℕ} (hkl : k ≤ l) (hne : (minmaxSet T l).Nonempty) : minmaxLevel T k ≤ minmaxLevel T l

Initializing...

(T : F →L[ℂ] F) {k l : ℕ} (hkl : k ≤ l) (hne : (minmaxSet T l).Nonempty) : minmaxLevel T k ≤ minmaxLevel T l · Prove2Me