English
If f is a uniform embedding, then we have two-way δ–ε control: (i) for every ε>0 there exists δ>0 with dist a b < δ ⇒ dist(f a) (f b) < ε; (ii) for every δ>0 there exists ε>0 with dist(f a) (f b) < ε ⇒ dist a b < δ.
Русский
Если f — равномерное вложение, то существует двусторонний контроль δ–ε: (i) для каждого ε>0 есть δ>0 such that dist(a,b)<δ ⇒ dist(f a, f b)<ε; (ii) для каждого δ>0 есть ε>0 such что dist(f a, f b)<ε ⇒ dist(a,b)<δ.
LaTeX
$$$\\text{IsUniformEmbedding}(f) \\Rightarrow \n\\Big( \\forall \\varepsilon>0, \\exists \\delta>0, \\forall a,b, dist(a,b)<\\delta \\Rightarrow dist(f(a),f(b))<\\varepsilon\\Big) \\\\n\\land \\\\ \\forall \\delta>0, \\exists \\varepsilon>0, \\forall a,b, dist(f(a),f(b))<\\varepsilon \\Rightarrow dist(a,b)<\\delta$$$
Lean4
/-- If a map between pseudometric spaces is a uniform embedding then the distance between `f x`
and `f y` is controlled in terms of the distance between `x` and `y`. -/
theorem controlled_of_isUniformEmbedding [PseudoMetricSpace β] {f : α → β} (h : IsUniformEmbedding f) :
(∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε) ∧
∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ :=
⟨uniformContinuous_iff.1 h.uniformContinuous, (isUniformEmbedding_iff.1 h).2.2⟩
