opNorm_le_of_lipschitz — Mathlib

English

If a bounded additive group homomorphism f is Lipschitz with constant K, then its operator norm is at most K.

Русский

Если отображение f как гомоморфизм группы ограничено и липшицево с константой K, то его операторная норма ≤ K.

LaTeX

$$$$ \text{LipschitzWith } K\ f \Rightarrow \|f\| \le K $$$$

Lean4

theorem opNorm_le_of_lipschitz {f : NormedAddGroupHom V₁ V₂} {K : ℝ≥0} (hf : LipschitzWith K f) : ‖f‖ ≤ K :=
  f.opNorm_le_bound K.2 fun x => by simpa only [dist_zero_right, map_zero] using hf.dist_le_mul x 0

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