Theorems · Theorem · general topology

isUniformEmbedding_of_spaced_out

∀ {β : Type v} [inst : UniformSpace β] {α : Type u_1} {f : α → β} {s : Set (β × β)},
  s ∈ uniformity β → (Pairwise fun x y => (f x, f y) ∉ s) → IsUniformEmbedding f

If a map f : α → β sends any two distinct points to point that are not related by a fixed s ∈ 𝓤 β, then f is a uniform embedding with respect to the discrete uniformity on α.

Defined in

Mathlib.Topology.UniformSpace.UniformEmbedding

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpace