English
In a uniform space (α, 𝓤 α), for every s ⊆ α × α, the closure of s equals the intersection of its V-thickening over all symmetric entourages V in 𝓤 α: closure(s) = ⋂_{V ∈ 𝓤 α, IsSymmetricRel V} V ○ s ○ V.
Русский
В равномерном пространстве (α, 𝓤 α) при любом S ⊆ α × α выполняется: closure(S) = ⋂_{V ∈ 𝓤 α, IsSymmetricRel V} V ○ S ○ V.
LaTeX
$$$\overline{s} = \bigcap_{V \in \{V \mid V \in 𝓤 α \land IsSymmetricRel V\}} V \circ s \circ V$$$
Lean4
theorem closure_eq_uniformity (s : Set <| α × α) : closure s = ⋂ V ∈ {V | V ∈ 𝓤 α ∧ IsSymmetricRel V}, V ○ s ○ V :=
by
ext ⟨x, y⟩
simp +contextual only [mem_closure_iff_nhds_basis (UniformSpace.hasBasis_nhds_prod x y), mem_iInter, mem_setOf_eq,
and_imp, mem_comp_comp, ← mem_inter_iff, inter_comm, Set.Nonempty]
