mem_codiscrete — Mathlib

English

Characterization of codiscrete membership via AccPt (accumulation point) for punctured principal neighborhoods.

Русский

Характеризация принадлежности кодискретности через AccPt в отношении пунктированных окружений.

LaTeX

$$$S \in codiscrete X \iff \forall x, \lnot AccPt(x, 𝓟 S^c).$$$

Lean4

theorem mem_codiscrete {S : Set X} : S ∈ codiscrete X ↔ ∀ x, Disjoint (𝓝[≠] x) (𝓟 Sᶜ) := by
  simp [codiscrete, mem_codiscreteWithin, compl_eq_univ_diff]

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