English
If a map f: β → α sends any two distinct points to points at distance at least ε>0, then f is a uniform embedding with respect to the bot (discrete) uniformity on β.
Русский
Если отображение f: β → α разделяет любые две точки расстоянием как минимум ε>0, то оно является равномерно вложением относительно дискретной униформности на β.
LaTeX
$$$ \text{isUniformEmbedding_bot_of_pairwise_le_dist } {f} {ε} (hf) : IsUniformEmbedding f$$$
Lean4
/-- Pull back a metric space structure by a uniform embedding. This is a version of
`MetricSpace.induced` useful in case if the domain already has a `UniformSpace` structure. -/
abbrev comapMetricSpace {α β} [UniformSpace α] [m : MetricSpace β] (f : α → β) (h : IsUniformEmbedding f) :
MetricSpace α :=
.replaceUniformity (.induced f h.injective m) h.comap_uniformity.symm
