[Nontrivial F] (T : F →L[ℂ] F) : (rayleighSet T).Nonempty
ProvedBookProof.ChapterSirkRitzSpectrum.rayleighSet_nonemptysirkspectral-theorytimepiece
Lean 4 theorem BookProof.ChapterSirkRitzSpectrum.rayleighSet_nonempty (module BookProof.ChapterSirkRitzSpectrum), source chapter BookProof/ChapterChapterSirkRitzSpectrum.lean.
Preamble
-- Generated from ChapterSirkRitzSpectrum.lean — theorem BookProof.ChapterSirkRitzSpectrum.rayleighSet_nonempty
import Mathlib
import Definitions.Def_ChapterSirkRitzSpectrum
open BookProof.ChapterSirkRitzSpectrum
noncomputable section
open Filter Topology RCLike ContinuousLinearMap ComplexOrder Pointwise
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]Formal statement
theorem BookProof.ChapterSirkRitzSpectrum.rayleighSet_nonempty [Nontrivial F] (T : F →L[ℂ] F) : (rayleighSet T).Nonempty := by sorry
Source