English
In a T0 space α, given an entourage V0 ∈ 𝓤 α, if a set s is spaced apart by V0 (i.e., no pair of distinct points of s are related by V0), then s is closed.
Русский
В T0-пространстве α, при данному entourage V0 ∈ 𝓤 α и множестве s, разнесённом по V0, множество s закрыто.
LaTeX
$$$[T0Space(α)]\ V_0 \in 𝓤(α) \Rightarrow (\forall s, \ Pairwise (x,y) \mapsto (x,y) \notin V_0) → IsClosed(s)$$$
Lean4
theorem isClosed_of_spaced_out [T0Space α] {V₀ : Set (α × α)} (V₀_in : V₀ ∈ 𝓤 α) {s : Set α}
(hs : s.Pairwise fun x y => (x, y) ∉ V₀) : IsClosed s :=
by
rcases comp_symm_mem_uniformity_sets V₀_in with ⟨V₁, V₁_in, V₁_symm, h_comp⟩
apply isClosed_of_closure_subset
intro x hx
rw [mem_closure_iff_ball] at hx
rcases hx V₁_in with ⟨y, hy, hy'⟩
suffices x = y by rwa [this]
apply eq_of_forall_symmetric
intro V V_in _
rcases hx (inter_mem V₁_in V_in) with ⟨z, hz, hz'⟩
obtain rfl : z = y := by
by_contra hzy
exact hs hz' hy' hzy (h_comp <| mem_comp_of_mem_ball V₁_symm (ball_inter_left x _ _ hz) hy)
exact ball_inter_right x _ _ hz
