(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

-- Generated from ChapterSirkRitzPerturbation.lean — theorem BookProof.RitzPerturbation.minmaxLevel_mono_form
import Mathlib
import Definitions.Def_ChapterSirkRitzPerturbation
open BookProof.RitzPerturbation








noncomputable section


open BookProof.RitzMinMax BookProof.ChapterSirkRitzSpectrum BookProof.HermiteGalerkin
open Filter Topology

variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]

theorem BookProof.RitzPerturbation.minmaxLevel_mono_form (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 := by sorry