orthogonalComplement_iSup_eigenspaces_eq_bot'

English

The iSup of all eigenspaces has an orthogonal complement which is the zero subspace.

Русский

Общая ортогональная компонента iSup эйгенпространств равна нулю.

LaTeX

$$$$ \left( \bigcup_{\mu} \mathrm{Eig}(T,\mu) \right)^{\perp} = \{0\}. $$$$

Lean4

theorem orthogonalComplement_iSup_eigenspaces_eq_bot' (hT : T.IsSymmetric) :
    (⨆ μ : Eigenvalues T, eigenspace T μ)ᗮ = ⊥ :=
  show (⨆ μ : { μ // eigenspace T μ ≠ ⊥ }, eigenspace T μ)ᗮ = ⊥ by
    rw [iSup_ne_bot_subtype, hT.orthogonalComplement_iSup_eigenspaces_eq_bot]

Похожие утверждения