edist_lt_top — Mathlib

English

For a Lipschitz function, the diameter of the image of a set is bounded by K times the diameter of the set.

Русский

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

LaTeX

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

Lean4

theorem edist_lt_top (hf : LipschitzWith K f) {x y : α} (h : edist x y ≠ ⊤) : edist (f x) (f y) < ⊤ :=
  (hf x y).trans_lt (by finiteness)

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