ofLipschitz_norm_le — Mathlib

English

For a group homomorphism f with Lipschitz bound K, the norm of its constructed normed map is at most K.

Русский

Для гомоморфизма f с липшицевой константой K норма конструктораNormedAddGroupHom не превышает K.

LaTeX

$$$$ \|\operatorname{ofLipschitz} f h\| \le K $$$$

Lean4

/-- If a bounded group homomorphism map is constructed from a group homomorphism via the constructor
`NormedAddGroupHom.ofLipschitz`, then its norm is bounded by the bound given to the constructor. -/
theorem ofLipschitz_norm_le (f : V₁ →+ V₂) {K : ℝ≥0} (h : LipschitzWith K f) : ‖ofLipschitz f h‖ ≤ K :=
  mkNormedAddGroupHom_norm_le f K.coe_nonneg _

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