starProjection_minimal — Mathlib

English

The projection of y onto U minimizes the distance to y among all points of U: ||y − P_U(y)|| = inf_{x ∈ U} ||y − x||.

Русский

Проекция y на U минимизирует расстояние до y среди всех точек U: ||y − P_U(y)|| = inf_{x ∈ U} ||y − x||.

LaTeX

$$||y - P_U(y)|| = \inf_{x \in U} ||y - x||.$$

Lean4

/-- The orthogonal projection of `y` on `U` minimizes the distance `‖y - x‖` for `x ∈ U`. -/
theorem starProjection_minimal {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (y : E) :
    ‖y - U.starProjection y‖ = ⨅ x : U, ‖y - x‖ :=
  by
  rw [starProjection_apply, U.norm_eq_iInf_iff_inner_eq_zero (Submodule.coe_mem _)]
  exact starProjection_inner_eq_zero _

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