exists_accPt_of_subset_isCompact — Mathlib

English

If s is infinite and contained in a compact set K, there exists x ∈ K that is an accumulation point of s with respect to the principal filter on s.

Русский

Если s бесконечно и содержится в компактном множестве K, существует точка x ∈ K, которая является точкой накопления для s в отношении главного фильтра на s.

LaTeX

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

Lean4

theorem exists_accPt_of_subset_isCompact {K : Set X} (hs : s.Infinite) (hK : IsCompact K) (hsub : s ⊆ K) :
    ∃ x ∈ K, AccPt x (𝓟 s) :=
  let ⟨x, hxK, hx⟩ := hs.exists_accPt_cofinite_inf_principal_of_subset_isCompact hK hsub
  ⟨x, hxK, hx.mono inf_le_right⟩

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