`BookProof.ChapterSchurIrreducible.cfc_ne_zero_of_mem_spectrum` [Nontrivial V] {T : V →L[ℂ] V} (hT : IsSelfAdjoint T) {f : ℝ → ℝ} (hf : Continuous f) {p : ℝ} (hp : p ∈ spectrum ℝ T

Proved

BookProof.ChapterSchurIrreducible.cfc_ne_zero_of_mem_spectrum

by leonardopedro · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterSchurIrreducible.

BookProof.ChapterSchurIrreducible.cfc_ne_zero_of_mem_spectrum [Nontrivial V] {T : V →L[ℂ] V} (hT : IsSelfAdjoint T) {f : ℝ → ℝ} (hf : Continuous f) {p : ℝ} (hp : p ∈ spectrum ℝ T) (hfp : f p ≠ 0) : cfc f T ≠ 0

Formalization note: Lean 4 identifier BookProof.ChapterSchurIrreducible.cfc_ne_zero_of_mem_spectrum.

Preamble

-- Generated from ChapterSchurIrreducible.lean — theorem BookProof.ChapterSchurIrreducible.cfc_ne_zero_of_mem_spectrum
import Definitions.Def_ChapterA
import Mathlib
import Definitions.Def_ChapterSchurIrreducible
open BookProof.ChapterSchurIrreducible


open scoped ComplexConjugate InnerProductSpace


open BookProof.ChapterA BookProof.ChapterA.System

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

Formal statement

theorem BookProof.ChapterSchurIrreducible.cfc_ne_zero_of_mem_spectrum [Nontrivial V] {T : V →L[ℂ] V} (hT : IsSelfAdjoint T)
    {f : ℝ → ℝ} (hf : Continuous f) {p : ℝ} (hp : p ∈ spectrum ℝ T) (hfp : f p ≠ 0) :
    cfc f T ≠ 0 := by sorry

View graph