English
A map f is a uniform embedding iff it is injective, uniformly continuous, and has the same δ–ε control as in the uniform inducing case, without loss of injectivity.
Русский
Отображение f является равномерным вложением тогда и только тогда, когда оно инъективно, равномерно непрерывно и обладает тем же δ–ε управлением, что и равномерная индукция.
LaTeX
$$$\\text{IsUniformEmbedding}(f) \\iff \\text{Injective}(f) \\land \\text{UniformContinuous}(f) \\land \\forall \\delta>0, \\exists \\varepsilon>0, \\forall a,b, dist(f(a),f(b))<\\varepsilon \\Rightarrow dist(a,b)<\\delta$$$
Lean4
nonrec theorem isUniformEmbedding_iff [PseudoMetricSpace β] {f : α → β} :
IsUniformEmbedding f ↔
Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ :=
by rw [isUniformEmbedding_iff, and_comm, isUniformInducing_iff]
