erealEquivReal — Mathlib

English

There is a measurable equivalence between the set of finite EReal numbers and ℝ.

Русский

Существует измеримое эквивалентное отображение между множеством конечных элементов EReal и ℝ.

LaTeX

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

Lean4

/-- The set of finite `EReal` numbers is `MeasurableEquiv` to `ℝ`. -/
def erealEquivReal : ({⊥, ⊤}ᶜ : Set EReal) ≃ᵐ ℝ :=
  EReal.neBotTopHomeomorphReal.toMeasurableEquiv

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