starProjection_eq_self_iff — Mathlib

English

The projection onto the whole space equals the identity: P_{⊤} = Id.

Русский

Проекция на все пространство равна тождественному отображению: P_{⊤} = Id.

LaTeX

$$P_{\top} = \mathrm{Id}.$$

Lean4

/-- A point equals its orthogonal projection if and only if it lies in the subspace. -/
theorem starProjection_eq_self_iff {v : E} : K.starProjection v = v ↔ v ∈ K :=
  by
  refine ⟨fun h => ?_, fun h => eq_starProjection_of_mem_of_inner_eq_zero h ?_⟩
  · rw [← h]
    simp
  · simp

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