English
A closure characterization using symmetric balls: x ∈ closure s iff for every symmetric V in the uniformity, (s ∩ ball x V) is nonempty.
Русский
Замыкание характеризуется через симметричные шары: x принадлежит closure s тогда и только тогда, когда для каждого симметричного V из равномерности, множесто (s ∩ ball x V) непусто.
LaTeX
$$$x \in \overline{s} \iff \forall V\in \mathcal U(\alpha), IsSymmetricRel V \rightarrow (s \cap \operatorname{ball}(x,V)).Nonempty$$$
Lean4
theorem mem_closure_iff_symm_ball {s : Set α} {x} :
x ∈ closure s ↔ ∀ {V}, V ∈ 𝓤 α → IsSymmetricRel V → (s ∩ ball x V).Nonempty := by
simp [mem_closure_iff_nhds_basis (hasBasis_nhds x), Set.Nonempty]