uniformContinuous — Mathlib

English

A Lipschitz function multiplies the diameter of a set by at most K.

Русский

Липшицева функция умножает диаметр множества не более чем на K.

LaTeX

$$$\text{ediam}(f''s) \le K \cdot \text{ediam}(s)$$$

Lean4

/-- A Lipschitz function is uniformly continuous. -/
protected theorem uniformContinuous (hf : LipschitzWith K f) : UniformContinuous f :=
  EMetric.uniformContinuous_iff.2 fun ε εpos =>
    ⟨ε / K, ENNReal.div_pos_iff.2 ⟨ne_of_gt εpos, ENNReal.coe_ne_top⟩, hf.edist_lt_of_edist_lt_div⟩

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