conj_starProjection — Mathlib

English

If T is self-adjoint, then compressing T to a subspace via its star projection remains self-adjoint.

Русский

Если T самосопряжённый, то сжатие T до подпространства через starProjection остаётся самосопряжённым.

LaTeX

$$$\\forall U\\,(h_T:\\IsSelfAdjoint T)\\implies IsSelfAdjoint(U^{\\starProjection} \\circ_L T \\circ_L U^{\\starProjection})$$$

Lean4

theorem conj_starProjection {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] :
    IsSelfAdjoint (U.starProjection ∘L T ∘L U.starProjection) :=
  by
  rw [← mul_def, ← mul_def, ← mul_assoc]
  exact hT.conjugate_self <| isSelfAdjoint_starProjection U

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