ltTopHomeomorphNNReal — Mathlib

English

The finite ENNReal numbers {a | a < ∞} are homeomorphic to NNReal.

Русский

Множество конечных ENNReal чисел {a | a < ∞} гомеоморфно NNReal.

LaTeX

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

Lean4

/-- The set of finite `ℝ≥0∞` numbers is homeomorphic to `ℝ≥0`. -/
def ltTopHomeomorphNNReal : {a | a < ∞} ≃ₜ ℝ≥0 :=
  by
  refine (Homeomorph.setCongr ?_).trans neTopHomeomorphNNReal
  simp only [lt_top_iff_ne_top]

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