exists_accPt_cofinite_inf_principal

English

In a compact space, every infinite subset s has a point x that is an accumulation point for the filter cofinite ∩ principal s.

Русский

В компактном пространстве любая бесконечная подмножество s имеет точку x, являющуюся точкой накопления для фильтра cofinit ∩ principal(s).

LaTeX

$$$\\exists x, AccPt(x, (cofinite \\cap \\mathcal{P}(s)))$$$

Lean4

theorem exists_accPt_cofinite_inf_principal [CompactSpace X] (hs : s.Infinite) : ∃ x, AccPt x (cofinite ⊓ 𝓟 s) := by
  simpa only [mem_univ, true_and] using
    hs.exists_accPt_cofinite_inf_principal_of_subset_isCompact isCompact_univ s.subset_univ

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