Theorems · Theorem · general topology

uniformity_hasBasis_open_symmetric

∀ {α : Type ua} [inst : UniformSpace α], (uniformity α).HasBasis (fun V => V ∈ uniformity α ∧ IsOpen V ∧ V.IsSymm) id

Open elements s : SetRel α α of 𝓤 α such that (x, y) ∈ s ↔ (y, x) ∈ s form a basis of 𝓤 α.

Defined in

Mathlib.Topology.UniformSpace.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

UniformSpace