exists_nhds_ne_inf_principal_neBot

English

If a subset s is compact and infinite, then s contains a limit point; that is, there exists z in s such that every neighborhood of z contains another point of s.

Русский

Если множество s компактно и бесконечно, то в s найдётся точка накопления: существует z ∈ s такая, что каждое окрестность z содержит другую точку из s.

LaTeX

$$$\IsCompact\,s \land s\text{ Infinite} \Rightarrow \exists z \in s, (\mathcal{N}[\neq] z \cap \mathcal{P}s).NeBot$$$

Lean4

theorem exists_nhds_ne_inf_principal_neBot (hs : IsCompact s) (hs' : s.Infinite) : ∃ z ∈ s, (𝓝[≠] z ⊓ 𝓟 s).NeBot :=
  hs'.exists_accPt_of_subset_isCompact hs Subset.rfl

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