English
A map between emetric spaces is a uniform embedding iff the edistance between f x and f y is controlled by the distance between x and y and conversely.
Русский
Отображение между эмметрическими пространствами является равномерной вложенностью тогда и только тогда, когда расстояние edist(f x, f y) управляется расстоянием edist x y, и наоборот.
LaTeX
$$IsUniformEmbedding f \iff (∀ ε > 0, ∃ δ > 0, ∀ {a b}, edist a b < δ → edist (f a) (f b) < ε) ∧ (∀ δ > 0, ∃ ε > 0, ∀ {a b}, edist (f a) (f b) < ε → edist a b < δ)$$
Lean4
/-- A map between emetric spaces is a uniform embedding if and only if the edistance between `f x`
and `f y` is controlled in terms of the distance between `x` and `y` and conversely. -/
theorem isUniformEmbedding_iff' [PseudoEMetricSpace β] {f : γ → β} :
IsUniformEmbedding f ↔
(∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧
∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ :=
by rw [isUniformEmbedding_iff_isUniformInducing, isUniformInducing_iff, uniformContinuous_iff]
