Theorems · Theorem · general topology

isClosed_of_spaced_out

∀ {α : Type u} [inst : UniformSpace α] [T0Space α] {V₀ : Set (α × α)},
  V₀ ∈ uniformity α → ∀ {s : Set α}, (s.Pairwise fun x y => (x, y) ∉ V₀) → IsClosed s

Defined in

Mathlib.Topology.UniformSpace.Separation

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpaceT0Space