eq_starProjection_of_mem_orthogonal'

English

If u = v + z with v ∈ K and z ∈ K^⊥, then the projection of u onto K is v.

Русский

Если u разложимо как u = v + z с v ∈ K и z ∈ K^⊥, то проекция u на K равна v.

LaTeX

$$If v ∈ K and z ∈ K^⊥ and u = v + z, then 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 z : E} (hv : v ∈ K) (hz : z ∈ Kᗮ) (hu : u = v + z) :
    K.starProjection u = v :=
  eq_starProjection_of_mem_orthogonal hv (by simpa [hu])

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