orthogonalProjection_eq_zero_iff — Mathlib

English

For v ∈ E, K.orthogonalProjection(v) = 0 if and only if v ∈ K^⊥.

Русский

Для v ∈ E нулевая ортогональная проекция равна тогда и только тогда, когда v ∈ K^⊥.

LaTeX

$$K.orthogonalProjection(v) = 0 ⇔ v ∈ K^{\perp}.$$

Lean4

@[simp]
theorem orthogonalProjection_eq_zero_iff {v : E} : K.orthogonalProjection v = 0 ↔ v ∈ Kᗮ :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ Subtype.eq <| eq_starProjection_of_mem_orthogonal (zero_mem _) ?_⟩
  · rw [← sub_zero v, ← coe_zero (p := K), ← h]
    exact sub_starProjection_mem_orthogonal (K := K) v
  · simpa

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