isSymmetricProjection_iff_eq_coe_starProjection

English

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

Русский

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

LaTeX

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

Lean4

theorem _root_.LinearMap.isSymmetricProjection_iff_eq_coe_starProjection {p : E →ₗ[𝕜] E} :
    p.IsSymmetricProjection ↔ ∃ (K : Submodule 𝕜 E) (_ : K.HasOrthogonalProjection), p = K.starProjection :=
  ⟨fun h ↦ ⟨LinearMap.range p, p.isSymmetricProjection_iff_eq_coe_starProjection_range.mp h⟩, by rintro ⟨_, _, rfl⟩;
    exact isSymmetricProjection_starProjection _⟩

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