Theorems · Theorem · general topology

union_mem_uniformity_sum

∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {a : SetRel α α},
  a ∈ uniformity α →
    ∀ {b : SetRel β β},
      b ∈ uniformity β → Prod.map Sum.inl Sum.inl '' a ∪ Prod.map Sum.inr Sum.inr '' b ∈ uniformity (α ⊕ β)

The union of an entourage of the diagonal in each set of a disjoint union is again an entourage of the diagonal.

Defined in

Mathlib.Topology.UniformSpace.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpace