le_mul_ediam_image — Mathlib

English

diameter is controlled under image by a Lipschitz constant: diam s ≤ K · diam (f''s).

Русский

Диаметр множества ≤ константа умноженная на диаметр образа под изображением f.

LaTeX

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

Lean4

theorem le_mul_ediam_image (hf : AntilipschitzWith K f) (s : Set α) : diam s ≤ K * diam (f '' s) :=
  (diam_mono (subset_preimage_image _ _)).trans (hf.ediam_preimage_le (f '' s))

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