English
A map is a uniform embedding if and only if it is injective, uniformly continuous, and for every δ>0 there exists ε>0 such that edist(a,b)<ε implies edist(f a, f b) < δ, and conversely with roles reversed.
Русский
Отображение является равномерно вложением если и только если оно инъективно, равномерно непрерывно и удовлетворяет ε-δ условиям на прообразе параметров.
LaTeX
$$$f: \alpha \to \beta$ isUniformEmbedding \iff (Injective f) \wedge UniformContinuous f \wedge ∀ δ>0, ∃ ε>0, ∀ {a,b}, edist(a,b)<ε \Rightarrow edist(f a,f b)<δ$.$$
Lean4
/-- ε-δ characterization of uniform embeddings on pseudoemetric spaces -/
nonrec theorem isUniformEmbedding_iff [PseudoEMetricSpace β] {f : α → β} :
IsUniformEmbedding f ↔
Function.Injective f ∧
UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ :=
(isUniformEmbedding_iff _).trans <| and_comm.trans <| Iff.rfl.and isUniformInducing_iff
