ediam_preimage_le — Mathlib

English

A map that is AntilipschitzWith and uniformly continuous is a uniform embedding.

Русский

Отображение, являющееся антилипшицевым и равномерно непрерывным, является равномерной вложенностью.

LaTeX

$$$IsUniformEmbedding(f)$$$

Lean4

theorem ediam_preimage_le (hf : AntilipschitzWith K f) (s : Set β) : diam (f ⁻¹' s) ≤ K * diam s :=
  diam_le fun x hx y hy => (hf x y).trans <| mul_le_mul_left' (edist_le_diam_of_mem (mem_preimage.1 hx) hy) K

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