(T : F →L[ℂ] F) (k : ℕ) : BddBelow (minmaxSet T k)

Open

BookProof.RitzMinMax.minmaxSet_bddBelow

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

timepiece

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

Preamble

-- Generated from ChapterSirkRitzMinMax.lean — theorem BookProof.RitzMinMax.minmaxSet_bddBelow
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.minmaxSet_bddBelow (T : F →L[ℂ] F) (k : ℕ) : BddBelow (minmaxSet T k) := by sorry

Source

https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterRitzMinMax.lean

View graph