orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero

English

The orthogonal projection of an element of Kᗮ onto K is zero.

Русский

Ортогональная проекция элемента из Kᗮ на K равна нулю.

LaTeX

$$$ K.orthogonalProjection(v) = 0 \quad \text{если } v \in K^{\perp} $$$

Lean4

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

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