exists_accPt_cofinite_inf_principal_of_subset_isCompact

English

If s is infinite, K is compact, and s ⊆ K, there exists x ∈ K that is an accumulation point of s with respect to the cofinite and principal-s filter.

Русский

Если s бесконечно, K компактно, и s ⊆ K, то найдётся точка x ∈ K, которая является пределом к точке от s относительно фильтра cofinit и principal(s).

LaTeX

$$$\\exists x \\in K, AccPt(x, (\\text{cofinite} \\sqcap \\mathcal{P}(s)))$$$

Lean4

theorem exists_accPt_cofinite_inf_principal_of_subset_isCompact {K : Set X} (hs : s.Infinite) (hK : IsCompact K)
    (hsub : s ⊆ K) : ∃ x ∈ K, AccPt x (cofinite ⊓ 𝓟 s) :=
  (@hK _ hs.cofinite_inf_principal_neBot (inf_le_right.trans <| principal_mono.2 hsub)).imp fun x hx ↦ by
    rwa [accPt_iff_clusterPt, inf_comm, inf_right_comm, (finite_singleton _).cofinite_inf_principal_compl]

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