eq_starProjection_of_mem_of_inner_eq_zero

English

If u ∈ E and v ∈ K satisfy ∀ w ∈ K, ⟨u − v, w⟩ = 0, then the orthogonal projection of u onto K equals v; i.e., P_K(u) = v.

Русский

Пусть u ∈ E и v ∈ K удовлетворяют ∀ w ∈ K, ⟨u − v, w⟩ = 0; тогда ортогональная проекция u на K равна v, то есть P_K(u) = v.

LaTeX

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

Lean4

/-- The orthogonal projection is the unique point in `K` with the
orthogonality property. -/
theorem eq_starProjection_of_mem_of_inner_eq_zero {u v : E} (hvm : v ∈ K) (hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0) :
    K.starProjection u = v :=
  eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero hvm hvo

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