English
From a uniform embedding, one gets two-way control: for every ε>0 there is δ>0 such that edist a b < δ implies edist(f a) (f b) < ε, and conversely with roles reversed for δ.
Русский
Из равномерного вложения следует двусторонний контроль: для каждого ε>0 существует δ>0 такой, что edist(a,b) < δ ⇒ edist(f a, f b) < ε, и наоборот в обратную сторону.
LaTeX
$$$f \text{ uniformEmbedding} \Rightarrow (\forall ε>0,\ exists δ>0, ∀ {a,b}, edist(a,b)<δ \Rightarrow edist(f a,f b)<ε) \wedge \forall δ>0, ∃ ε>0, ∀{a,b}, edist(f a,f b)<ε \Rightarrow edist(a,b)<δ$$$
Lean4
/-- If a map between pseudoemetric spaces is a uniform embedding then the edistance between `f x`
and `f y` is controlled in terms of the distance between `x` and `y`.
In fact, this lemma holds for a `IsUniformInducing` map.
TODO: generalize? -/
theorem controlled_of_isUniformEmbedding [PseudoEMetricSpace β] {f : α → β} (h : 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 < δ :=
⟨uniformContinuous_iff.1 h.uniformContinuous, (isUniformEmbedding_iff.1 h).2.2⟩
