orthogonalProjection_orthogonal_apply_eq_zero

English

The orthogonal projection onto K of any vector in K is the vector itself.

Русский

Ортогональная проекция на K любого вектора из K возвращает сам вектор.

LaTeX

$$$ \forall v \in K,\; \mathrm{orthogonalProjection}_K(v) = v $$$

Lean4

/-- The orthogonal projection onto `Kᗮ` of an element of `K` is zero. -/
theorem orthogonalProjection_orthogonal_apply_eq_zero [Kᗮ.HasOrthogonalProjection] {v : E} (hv : v ∈ K) :
    Kᗮ.orthogonalProjection v = 0 :=
  orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero (K.le_orthogonal_orthogonal hv)

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