starProjection_inner_eq_zero — Mathlib

English

Let K be a subspace of E with an orthogonal projection P_K. Then for every v in E and every w in K, the inner product ⟨v − P_K v, w⟩ equals 0.

Русский

Пусть K является подпространством E с ортогональной проекцией P_K. Тогда для каждого v ∈ E и каждого w ∈ K выполнено ⟨v − P_K v, w⟩ = 0.

LaTeX

$$$\forall v \in E, \forall w \in K, \langle v - P_K(v), w \rangle = 0.$$$

Lean4

/-- The characterization of the orthogonal projection. -/
@[simp]
theorem starProjection_inner_eq_zero (v : E) : ∀ w ∈ K, ⟪v - K.starProjection v, w⟫ = 0 :=
  orthogonalProjectionFn_inner_eq_zero v

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