ultrafilter_isClosed_basic — Mathlib

English

Let s be a subset of α. The basic closed set corresponding to s in the ultrafilter topology is the collection of ultrafilters that contain s; such sets are closed in Ultrafilter α.

Русский

Пусть s ⊆ α. Множество всех ультрафильтров u на α, которые содержат s, замкнутое в пространстве Ultrafilter α.

LaTeX

$$$IsClosed\{u : Ultrafilter\ α \mid s \in u\}$$$

Lean4

/-- The basic open sets for the topology on ultrafilters are also closed. -/
theorem ultrafilter_isClosed_basic (s : Set α) : IsClosed {u : Ultrafilter α | s ∈ u} :=
  by
  rw [← isOpen_compl_iff]
  convert ultrafilter_isOpen_basic sᶜ using 1
  ext u
  exact Ultrafilter.compl_mem_iff_notMem.symm

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