(T T' : F →L[ℂ] F) (k : ℕ) (hle : ∀ x : F, rayleighVal T x ≤ rayleighVal T' x) (hne : (minmaxSet T' k).Nonempty) : minmaxLevel T k ≤ minmaxLevel T' k

Initializing...

(T T' : F →L[ℂ] F) (k : ℕ) (hle : ∀ x : F, rayleighVal T x ≤ rayleighVal T' x) (hne : (minmaxSet T' k).Nonempty) : minmaxLevel T k ≤ minmaxLevel T' k · Prove2Me