starProjection_isSymmetric — Mathlib

English

A linear projection p is symmetric if and only if it is the orthogonal projection onto its range.

Русский

Линейная проекция p симметрична тогда и только тогда, когда она является ортогональной проекцией на своё образ.

LaTeX

$$$ p.IsSymmetricProjection \iff \exists K\ (K.HasOrthogonalProjection)\, (p = K.starProjection). $$$

Lean4

/-- The orthogonal projection is symmetric. -/
theorem starProjection_isSymmetric [K.HasOrthogonalProjection] : (K.starProjection : E →ₗ[𝕜] E).IsSymmetric :=
  inner_starProjection_left_eq_right K

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