orthogonalProjection_orthogonalComplement_singleton_eq_zero

English

For any nonzero vector v, the orthogonal projection of v onto the orthogonal complement of its span is zero.

Русский

Для любого ненулевого вектора v ортогональная проекция v на ортогональное дополнение линейной оболочки {v} равна нулю.

LaTeX

$$$ P_{(\operatorname{span}\{v\})^{\perp}}(v) = 0. $$$

Lean4

/-- The orthogonal projection onto `(𝕜 ∙ v)ᗮ` of `v` is zero. -/
theorem orthogonalProjection_orthogonalComplement_singleton_eq_zero (v : E) : (𝕜 ∙ v)ᗮ.orthogonalProjection v = 0 :=
  orthogonalProjection_orthogonal_apply_eq_zero (Submodule.mem_span_singleton_self v)

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