ultrafilter_isOpen_basic — Mathlib

English

For any subset s of α, the set {u ∈ Ultrafilter α : s ∈ u} is an open set in Ultrafilter α.

Русский

Для любого подмножества s из α множество {u ∈ Ultrafilter α : s ∈ u} открыто в Ultrafilter α.

LaTeX

$$$\\{u:\\mathrm{Ultrafilter}(\\alpha)\\;|\\; s\\in u\\}$ is open in Ultrafilter α.$$

Lean4

/-- The basic open sets for the topology on ultrafilters are open. -/
theorem ultrafilter_isOpen_basic (s : Set α) : IsOpen {u : Ultrafilter α | s ∈ u} :=
  ultrafilterBasis_is_basis.isOpen ⟨s, rfl⟩

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