topologicalSpace — Mathlib

English

The topology on Ultrafilter α is defined as the generated topology from the basis ultrafilterBasis α.

Русский

Топология на Ultrafilter α задаётся как порождённая топология от базиса ultrafilterBasis α.

LaTeX

$$$\\text{topologicalSpace}(\\mathrm{Ultrafilter}(\\alpha))=\\text{TopologicalSpace.generateFrom}(\\mathrm{ultrafilterBasis}(\\alpha)).$$$

Lean4

instance topologicalSpace : TopologicalSpace (Ultrafilter α) :=
  TopologicalSpace.generateFrom (ultrafilterBasis α)

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