Theorems · Theorem · general topology

Metric.isUniformEmbedding_bot_of_pairwise_le_dist

∀ {α : Type u} [inst : PseudoMetricSpace α] {β : Type u_2} {ε : ℝ},
  0 < ε → ∀ {f : β → α}, (Pairwise fun x y => ε ≤ dist (f x) (f y)) → IsUniformEmbedding f

If f : β → α sends any two distinct points to points at distance at least ε > 0, then f is a uniform embedding with respect to the discrete uniformity on β.

Defined in

Mathlib.Topology.MetricSpace.Basic

Cited by

4 results in Mathlib

Foundations

Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpace