ultrafilterBasis — Mathlib

English

Basis for the topology on Ultrafilter α is the collection of sets {u ∈ Ultrafilter α : s ∈ u} as s runs over all subsets s ⊆ α.

Русский

Базис топологии над Ultrafilter α задаётся множеством {u ∈ Ultrafilter α : s ∈ u} при всех подмножествах s ⊆ α.

LaTeX

$$$\\mathrm{ultrafilterBasis}(\\alpha)=\\{\\{u:\\mathrm{Ultrafilter}(\\alpha): s\\in u\\}: s\\subseteq\\alpha\\}\\,.$$$

Lean4

/-- Basis for the topology on `Ultrafilter α`. -/
def ultrafilterBasis (α : Type u) : Set (Set (Ultrafilter α)) :=
  range fun s : Set α ↦ {u | s ∈ u}

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