mul_edist_le — Mathlib

English

A Lipschitz function preserves a bound on the image diameter; a variant of the previous bound.

Русский

Липшицева функция сохраняет ограничение диаметра образа.

LaTeX

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

Lean4

theorem mul_edist_le (h : LipschitzWith K f) (x y : α) : (K⁻¹ : ℝ≥0∞) * edist (f x) (f y) ≤ edist x y :=
  by
  rw [mul_comm, ← div_eq_mul_inv]
  exact ENNReal.div_le_of_le_mul' (h x y)

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