Theorems · Theorem · general topology

uniformity_prod

∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β],
  uniformity (α × β) =
    Filter.comap (fun p => (p.1.1, p.2.1)) (uniformity α) ⊓ Filter.comap (fun p => (p.1.2, p.2.2)) (uniformity β)

Defined in

Mathlib.Topology.UniformSpace.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpace