Theorems · Theorem · general topology

comp_symm_of_uniformity

∀ {α : Type ua} [inst : UniformSpace α] {s : SetRel α α},
  s ∈ uniformity α → ∃ t ∈ uniformity α, (∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t) ∧ SetRel.comp t t ⊆ s

Defined in

Mathlib.Topology.UniformSpace.Defs

Cited by

7 results in Mathlib

Foundations

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

Assumes

UniformSpace