lipschitzWith_orthogonalProjection

English

The orthogonal projection onto a closed subspace is 1-Lipschitz.

Русский

Ортогональная проекция на замкнутое подпредпространство является 1-Липшицевой.

LaTeX

$$$ \mathrm{LipschitzWith}\ 1\ (\mathrm{orthogonalProjection}\ K) $$$

Lean4

/-- The orthogonal projection onto a closed subspace is a `1`-Lipschitz map. -/
theorem lipschitzWith_orthogonalProjection : LipschitzWith 1 (orthogonalProjection K) :=
  ContinuousLinearMap.lipschitzWith_of_opNorm_le (orthogonalProjection_norm_le K)

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