instTopologicalSpace — Mathlib

English

The topology on ENNReal = ℝ≥0∞ is the order topology coming from its natural preorder.

Русский

Топология на ENNReal = ℝ≥0∞ задаётся топологией порядка, порождаемой естественным иерархическим порядком.

LaTeX

$$$\\tau_{\\mathrm{ord}}(\\mathbb{R}_{\\ge 0}^{\\infty}) = \\text{order topology on } \\mathbb{R}_{\\ge 0}^{\\infty}$$$

Lean4

/-- Topology on `ℝ≥0∞`.

Note: this is different from the `EMetricSpace` topology. The `EMetricSpace` topology has
`IsOpen {∞}`, while this topology doesn't have singleton elements. -/
instance : TopologicalSpace ℝ≥0∞ :=
  Preorder.topology ℝ≥0∞

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