orthogonalProjection_orthogonalProjection

English

Applying the orthogonal projection twice yields the same result as once.

Русский

Повторное применение ортогональной проекции дает тот же результат, что и первое.

LaTeX

$$$ \operatorname{orthogonalProjection} s (\operatorname{orthogonalProjection} s p) = \operatorname{orthogonalProjection} s p $$$

Lean4

/-- Orthogonal projection is idempotent. -/
theorem orthogonalProjection_orthogonalProjection (s : AffineSubspace ℝ P) [Nonempty s]
    [s.direction.HasOrthogonalProjection] (p : P) :
    orthogonalProjection s (orthogonalProjection s p) = orthogonalProjection s p :=
  orthogonalProjection_mem_subspace_eq_self ((orthogonalProjection s) p)

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