isSelfAdjoint_starProjection — Mathlib

English

The orthogonal projection onto a subspace is a self-adjoint (Hermitian) operator.

Русский

Орthогональная проекция на подпространство является самосопряжённым оператором.

LaTeX

$$$\\text{IsSelfAdjoint}(U^{\\star\\text{Projection}})$$$

Lean4

/-- The orthogonal projection is self-adjoint. -/
@[simp]
theorem _root_.isSelfAdjoint_starProjection (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] :
    IsSelfAdjoint U.starProjection :=
  U.starProjection_isSymmetric.isSelfAdjoint

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