instTopologicalSpace — Mathlib

English

The extended natural numbers ℕ∞ are equipped with the order topology, i.e., the topology generated by the order on ℕ∞.

Русский

Расширенные натуральные числа ℕ∞ имеют топологию порядка, то есть топологию, порожденную по отношению порядка на ℕ∞.

LaTeX

$$$$\\mathcal{T}_{\\mathbb{N}_{\\infty}} = \\operatorname{Preorder.topology}(\\mathbb{N}_{\\infty}).$$$$

Lean4

/-- Topology on `ℕ∞`.

Note: this is different from the `EMetricSpace` topology. The `EMetricSpace` topology has
`IsOpen {∞}`, but all neighborhoods of `∞` in `ℕ∞` contain infinite intervals.
-/
instance : TopologicalSpace ℕ∞ :=
  Preorder.topology ℕ∞

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