neTopHomeomorphNNReal — Mathlib

English

The set {a | a ≠ ∞} is homeomorphic to ℝ≥0 via neTopEquivNNReal.

Русский

Множество {a | a ≠ ∞} гомеоморфно ℝ≥0 через neTopEquivNNReal.

LaTeX

$$$\\{a \\in \\mathbb{R}_{\\ge 0}^{\\infty} \\mid a \\neq \\infty\\} \\cong_{t} \\mathbb{R}_{\\ge 0}$$$

Lean4

/-- The set of finite `ℝ≥0∞` numbers is homeomorphic to `ℝ≥0`. -/
def neTopHomeomorphNNReal : {a | a ≠ ∞} ≃ₜ ℝ≥0
    where
  toEquiv := neTopEquivNNReal
  continuous_toFun := continuousOn_iff_continuous_restrict.1 continuousOn_toNNReal
  continuous_invFun := continuous_coe.subtype_mk _

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