ofLipschitz — Mathlib

English

Two normed add-group morphisms are equal iff their underlying functions are equal.

Русский

Два нормированных аддитивных гомоморфизма равны тогда и только тогда, когда их функциональные реализации равны.

LaTeX

$$$f=g \\iff (f:V_1\\to V_2)=(g)$$$

Lean4

/-- A Lipschitz continuous additive homomorphism is a normed additive group homomorphism. -/
def ofLipschitz (f : V₁ →+ V₂) {K : ℝ≥0} (h : LipschitzWith K f) : NormedAddGroupHom V₁ V₂ :=
  f.mkNormedAddGroupHom K fun x ↦ by simpa only [map_zero, dist_zero_right] using h.dist_le_mul x 0

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