starProjection_apply_eq_zero_iff — Mathlib

English

The starProjection of v onto (span{v})⊥ is zero.

Русский

Звёздочная проекция v на (span{v})⊥ равна нулю.

LaTeX

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

Lean4

theorem starProjection_apply_eq_zero_iff [K.HasOrthogonalProjection] {v : E} : K.starProjection v = 0 ↔ v ∈ Kᗮ :=
  by
  refine ⟨fun h w hw => ?_, fun hv => ?_⟩
  · rw [← starProjection_eq_self_iff.mpr hw, inner_starProjection_left_eq_right, h, inner_zero_right]
  · simp [starProjection_apply, orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero hv]

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