isOpen_iff_ultrafilter' — Mathlib

English

In a compact Hausdorff space, a set U is open iff for every ultrafilter F, if lim F ∈ U then U ∈ F.

Русский

В компактном Хаусдорфовом пространстве множество U открыто тогда и только тогда, когда для любого ультрафильтра F, если lim F ∈ U, то U ∈ F.

LaTeX

$$$\\text{IsOpen}(U) \\iff \\forall F : Ultrafilter X, F.lim \\in U \\rightarrow U \\in F.1$$$

Lean4

theorem isOpen_iff_ultrafilter' [CompactSpace X] (U : Set X) : IsOpen U ↔ ∀ F : Ultrafilter X, F.lim ∈ U → U ∈ F.1 :=
  by
  rw [isOpen_iff_ultrafilter]
  refine ⟨fun h F hF => h F.lim hF F F.le_nhds_lim, ?_⟩
  intro cond x hx f h
  rw [← Ultrafilter.lim_eq_iff_le_nhds.2 h] at hx
  exact cond _ hx

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