exists_accPt_principal — Mathlib

English

In a compact space, any infinite subset s has a point x that is an accumulation point of s in the principal filter on s.

Русский

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

LaTeX

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

Lean4

theorem exists_accPt_principal [CompactSpace X] (hs : s.Infinite) : ∃ x, AccPt x (𝓟 s) :=
  hs.exists_accPt_cofinite_inf_principal.imp fun _x hx ↦ hx.mono inf_le_right

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