Theorems · Theorem · general topology

Filter.HasBasis.mem_uniformity_iff

∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {p : β → Prop} {s : β → SetRel α α},
  (uniformity α).HasBasis p s → ∀ {t : SetRel α α}, t ∈ uniformity α ↔ ∃ i, p i ∧ ∀ (a b : α), (a, b) ∈ s i → (a, b) ∈ t

Defined in

Mathlib.Topology.UniformSpace.Basic

Cited by

4 results in Mathlib

Foundations

Depth 8 from the axioms · uses propext, Quot.sound

Assumes

UniformSpace