starProjection_apply — Mathlib

English

The star projection and the orthogonal projection agree when restricted to a subspace with a HasOrthogonalProjection.

Русский

Star-проекция и ортогональная проекция совпадают при ограничении к подпространству, имеющему HasOrthogonalProjection.

LaTeX

$$U.starProjection = U.orthogonalProjection$$

Lean4

theorem starProjection_apply (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (v : E) :
    U.starProjection v = U.orthogonalProjection v :=
  rfl

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