eq_starProjection_of_mem_orthogonal

English

A point u ∈ E for which v ∈ K and ∀ w ∈ K, ⟨u − v, w⟩ = 0 must satisfy P_K(u) = v.

Русский

Тогда, когда существует v ∈ K и ∀ w ∈ K, ⟨u − v, w⟩ = 0, обязана выполняться 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

/-- A point in `K` with the orthogonality property (here characterized in terms of `Kᗮ`) must be the
orthogonal projection. -/
theorem eq_starProjection_of_mem_orthogonal {u v : E} (hv : v ∈ K) (hvo : u - v ∈ Kᗮ) : K.starProjection u = v :=
  eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero hv <| (Submodule.mem_orthogonal' _ _).1 hvo

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