Theorems · Theorem · general topology

IsUniformInducing.comap_uniformity

∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing f → Filter.comap (fun x => (f x.1, f x.2)) (uniformity β) = uniformity α

The uniformity filter on the domain is the pullback of the uniformity filter on the codomain under Prod.map f f.

Defined in

Mathlib.Topology.UniformSpace.Defs

Cited by

22 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpace