Theorems · Theorem · general topology

uniformity_prod_eq_prod

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

Defined in

Mathlib.Topology.UniformSpace.Basic

Cited by

9 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpace