isClosed_of_spaced_out

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

This theorem states that for any type `α` equipped with a uniform space structure and an additional T0Space structure, given a set `V₀` of pairs from `α` that belongs to the uniformity of `α`, if for any set `s` of `α`, all distinct pairs `(x, y)` from `s` do not belong to `V₀` (property defined by the `Set.Pairwise` definition), then the set `s` is a closed set. In other words, it says that if all distinct pairs of elements from a set are 'spaced out' (i.e., not in a certain set related to the uniformity structure), then the original set is closed in the topology induced by the uniform space.

More concisely: Given a T0 space `α` with uniformity structure, a set `V₀` in its uniformity, if for every set `s`, all distinct pairs `(x, y)` from `s` are not in `V₀`, then `s` is closed.