Theorems · Theorem · general topology

nhdset_of_mem_uniformity

∀ {α : Type ua} [inst : UniformSpace α] {d : SetRel α α} (s : SetRel α α),
  d ∈ uniformity α → ∃ t, IsOpen t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}

Defined in

Mathlib.Topology.UniformSpace.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

UniformSpace