(T : F →L[ℂ] F) : minmaxSet T 0 = rayleighSet T
OpenBookProof.RitzMinMax.minmaxSet_zero_eq_rayleighSettimepiece
Lean 4 theorem BookProof.RitzMinMax.minmaxSet_zero_eq_rayleighSet (module BookProof.RitzMinMax), source chapter BookProof/ChapterRitzMinMax.lean.
Preamble
-- Generated from ChapterSirkRitzMinMax.lean — theorem BookProof.RitzMinMax.minmaxSet_zero_eq_rayleighSet
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_zero_eq_rayleighSet (T : F →L[ℂ] F) : minmaxSet T 0 = rayleighSet T := by sorry
Source