English
Let α and β be uniform spaces whose uniformities admit bases (p, s) on α and (p', s') on β. For a map f : α → β, f is a uniform embedding if and only if it is injective, uniformly continuous, and for every index j with p(j) there exists i with p'(i) such that for all x,y, if (f x, f y) ∈ s'_i then (x, y) ∈ s_j.
Русский
Пусть α и β — равномерные пространства, чьи равномерности имеют базисы (p, s) на α и (p', s') на β. Для отображения f : α → β отображение f является равномерным вложением тогда и только тогда, когда оно инъективно, равномерно непрерывно, и для каждого индекса j с p(j) существует i с p'(i), такое что для всех x, y выполняется: (f x, f y) ∈ s'_i ⇒ (x, y) ∈ s_j.
LaTeX
$$$\\displaystyle \\text{IsUniformEmbedding}(f)\\;\\Longleftrightarrow\\; \\Big( \\text{Injective}(f) \\land \\text{UniformContinuous}(f) \\land \\forall j\\, (p(j) \\Rightarrow \\exists i\\, (p'(i) \\land \\forall x,y\\, ((f x,f y) \\in s' i) \\Rightarrow (x,y) \\in s j))\\Big)$$$
Lean4
theorem isUniformEmbedding_iff {ι ι'} {p : ι → Prop} {p' : ι' → Prop} {s s'} (h : (𝓤 α).HasBasis p s)
(h' : (𝓤 β).HasBasis p' s') {f : α → β} :
IsUniformEmbedding f ↔
Injective f ∧ UniformContinuous f ∧ (∀ j, p j → ∃ i, p' i ∧ ∀ x y, (f x, f y) ∈ s' i → (x, y) ∈ s j) :=
by simp only [h.isUniformEmbedding_iff' h', h.uniformContinuous_iff h']
