orthogonalFamily_eigenspaces' — Mathlib

English

The orthogonal complement of the sum of all eigenspaces is an invariant subspace for the operator.

Русский

Ортогональное дополнение сумм собственных подпространств является инвариантным подпространством для оператора.

LaTeX

$$$$ (\bigoplus_{\mu} \mathrm{Eig}(T,\mu))^{\perp} \text{ is T-invariant}. $$$$

Lean4

theorem orthogonalFamily_eigenspaces' (hT : T.IsSymmetric) :
    OrthogonalFamily 𝕜 (fun μ : Eigenvalues T => eigenspace T μ) fun μ => (eigenspace T μ).subtypeₗᵢ :=
  hT.orthogonalFamily_eigenspaces.comp Subtype.coe_injective

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