Theorems · Theorem · general topology

comap_uniformity_of_spaced_out

∀ {β : Type v} [inst : UniformSpace β] {α : Type u_1} {f : α → β} {s : Set (β × β)},
  s ∈ uniformity β →
    (Pairwise fun x y => (f x, f y) ∉ s) → Filter.comap (Prod.map f f) (uniformity β) = Filter.principal SetRel.id

If a map f : α → β sends any two distinct points to point that are not related by a fixed s ∈ 𝓤 β, then f is uniform inducing with respect to the discrete uniformity on α: the preimage of 𝓤 β under Prod.map f f is the principal filter generated by the diagonal in α × α.

Defined in

Mathlib.Topology.UniformSpace.UniformEmbedding

Cited by

1 results in Mathlib

Foundations

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

Assumes

UniformSpace