Theorems · Theorem · general topology

entourageProd_mem_uniformity

∀ {α : Type ua} {β : Type ub} [t₁ : UniformSpace α] [t₂ : UniformSpace β] {u : SetRel α α} {v : SetRel β β},
  u ∈ uniformity α → v ∈ uniformity β → entourageProd u v ∈ uniformity (α × β)

Defined in

Mathlib.Topology.UniformSpace.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpace