orthogonalProjection_eq_self_iff — Mathlib

English

The projection of p onto s equals p if and only if p lies in s.

Русский

Проекция точки p на s равна самой точке p тогда и только тогда, когда p ∈ s.

LaTeX

$$$ \uparrow(\operatorname{orthogonalProjection} s p) = p \iff p \in s $$$

Lean4

/-- A point equals its orthogonal projection if and only if it lies in
the subspace. -/
theorem orthogonalProjection_eq_self_iff {s : AffineSubspace ℝ P} [Nonempty s] [s.direction.HasOrthogonalProjection]
    {p : P} : ↑(orthogonalProjection s p) = p ↔ p ∈ s :=
  by
  constructor
  · exact fun h => h ▸ orthogonalProjection_mem p
  · intro h
    have hp : p ∈ (s : Set P) ∩ mk' p s.directionᗮ := ⟨h, self_mem_mk' p _⟩
    rw [inter_eq_singleton_orthogonalProjection p] at hp
    symm
    exact hp

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