mem_codiscrete_accPt — Mathlib

English

Equivalence of codiscrete membership with a pointwise condition on AccPt for complements.

Русский

Эквивалентность принадлежности codiscrete с точечным условием AccPt для дополнений.

LaTeX

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

Lean4

theorem mem_codiscrete_accPt {S : Set X} : S ∈ codiscrete X ↔ ∀ x, ¬AccPt x (𝓟 Sᶜ) := by
  simp only [mem_codiscrete, disjoint_iff, AccPt, not_neBot]

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