starProjection_orthogonalComplement_singleton_eq_zero

English

The projection onto the orthogonal complement of the span of v (via the starProjection) of v is zero.

Русский

Проекция на ортогональное дополнение спана от вектора v (звёздочная проекция) вектора v равна нулю.

LaTeX

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

Lean4

theorem starProjection_orthogonalComplement_singleton_eq_zero (v : E) : (𝕜 ∙ v)ᗮ.starProjection v = 0 :=
  by
  rw [starProjection_apply, coe_eq_zero]
  exact orthogonalProjection_orthogonalComplement_singleton_eq_zero v

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