Prove2Me

(T : F →L[ℂ] F) (W : Submodule ℂ F) (k : ℕ) (hne : (minmaxSetIn T W k).Nonempty) : minmaxLevel T k ≤ minmaxLevelIn T W k

Open
BookProof.RitzMinMax.minmaxLevel_le_minmaxLevelIn

by leonardopedro · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

timepiece

Lean 4 theorem BookProof.RitzMinMax.minmaxLevel_le_minmaxLevelIn (module BookProof.RitzMinMax), source chapter BookProof/ChapterRitzMinMax.lean.

Preamble
-- Generated from ChapterSirkRitzMinMax.lean — theorem BookProof.RitzMinMax.minmaxLevel_le_minmaxLevelIn
import Mathlib
import Definitions.Def_ChapterSirkRitzMinMax
open BookProof.RitzMinMax









noncomputable section


open BookProof.HermiteGalerkin BookProof.ChapterSirkRitzSpectrum
open Filter Topology

variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
Formal statement
theorem BookProof.RitzMinMax.minmaxLevel_le_minmaxLevelIn (T : F →L[ℂ] F) (W : Submodule ℂ F) (k : ℕ)
    (hne : (minmaxSetIn T W k).Nonempty) :
    minmaxLevel T k ≤ minmaxLevelIn T W k := by sorry
Source
https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterRitzMinMax.lean

View graph