neTopBotEquivReal — Mathlib

English

The non-top non-bottom part of EReal is equivalent to Real numbers.

Русский

Множество элементов EReal, исключая верхний и нижний пределы, эквивалентно множеству вещественных чисел.

LaTeX

$$$ \{ x \\in \mathrm{EReal} : x \neq \top, x \neq \bot \} \simeq \mathbb{R} $$$

Lean4

/-- The set of numbers in `EReal` that are not equal to `±∞` is equivalent to `ℝ`. -/
def neTopBotEquivReal : ({⊥, ⊤}ᶜ : Set EReal) ≃ ℝ
    where
  toFun x := EReal.toReal x
  invFun x := ⟨x, by simp⟩
  left_inv := fun ⟨x, hx⟩ => by
    lift x to ℝ
    · simpa [not_or, and_comm] using hx
    · simp
  right_inv x := by simp

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