lipschitzOnWith_iff_norm_div_le — Mathlib

English

A homomorphism of semnormed groups is Lipschitz if there exists C such that ‖f x‖ ≤ C‖x‖ for all x.

Русский

Гомоморфизм полуметрических групп является липшицевым, если существует константа C, такая что ‖f(x)‖ ≤ C‖x‖ для всех x.

LaTeX

$$$\\exists C \\in \\mathbb{R},\\ (\\forall x, \\|f(x)\\| \\le C \\|x\\|) \\Rightarrow \\text{f is Lipschitz with constant } C$$$

Lean4

@[to_additive]
theorem lipschitzOnWith_iff_norm_div_le {f : E → F} {C : ℝ≥0} :
    LipschitzOnWith C f s ↔ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ‖f x / f y‖ ≤ C * ‖x / y‖ := by
  simp only [lipschitzOnWith_iff_dist_le_mul, dist_eq_norm_div]

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