neBotTopHomeomorphReal — Mathlib

English

The finite part of EReal, namely ({⊥, ⊤}ᶜ), is homeomorphic to ℝ.

Русский

Конечная часть EReal, т.е. ({⊥, ⊤}ᶜ), гомоморфна к ℝ.

LaTeX

$$$({\\perp,\\top}^{c})\\simeq_{T} \\mathbb{R}$$$

Lean4

/-- The set of finite `EReal` numbers is homeomorphic to `ℝ`. -/
def neBotTopHomeomorphReal : ({⊥, ⊤}ᶜ : Set EReal) ≃ₜ ℝ
    where
  toEquiv := neTopBotEquivReal
  continuous_toFun := continuousOn_iff_continuous_restrict.1 continuousOn_toReal
  continuous_invFun := continuous_coe_real_ereal.subtype_mk _

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