ultrafilter_le_nhds_infty — Mathlib

English

For an ultrafilter f on OnePoint X, f converges to ∞ iff it excludes the images of all closed compact subsets of X.

Русский

Для ультрафильтра f на OnePoint X f сходится к ∞ тогда, когда он не содержит образов всех замкнуто-компактных подмножеств X.

LaTeX

$$$\forall f : Ultrafilter(OnePoint X),\ f \le 𝓝(∞) \Leftrightarrow \forall s \subset X, IsClosed s \land IsCompact s \rightarrow \lnot (\uparrow '' s) \in f$$$

Lean4

theorem ultrafilter_le_nhds_infty {f : Ultrafilter (OnePoint X)} :
    (f : Filter (OnePoint X)) ≤ 𝓝 ∞ ↔ ∀ s : Set X, IsClosed s → IsCompact s → (↑) '' s ∉ f := by
  simp only [le_nhds_infty, ← compl_image_coe, Ultrafilter.mem_coe, Ultrafilter.compl_mem_iff_notMem]

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