le_nhds_lim — Mathlib

English

For a compact space X, any ultrafilter F on X satisfies that the underlying filter is contained in the neighborhood filter of its limit point lim F.

Русский

Для компактного пространства X любой ультрафильтр F на X удовлетворяет, что базовый фильтр F ⊆ 𝓝(лимит F).

LaTeX

$$$F \le 𝓝(\lim F)$$$

Lean4

nonrec theorem le_nhds_lim [CompactSpace X] (F : Ultrafilter X) : ↑F ≤ 𝓝 F.lim :=
  by
  rcases isCompact_univ.ultrafilter_le_nhds F (by simp) with ⟨x, -, h⟩
  exact le_nhds_lim ⟨x, h⟩

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