mem_closure_iff_symm_ball — Mathlib

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]

Похожие утверждения