The extended real numbers

This file defines EReal, ℝ with a top element ⊤ and a bottom element ⊥, implemented as WithBot (WithTop ℝ).

EReal is a CompleteLinearOrder, deduced by typeclass inference from the fact that WithBot (WithTop L) completes a conditionally complete linear order L.

Coercions from ℝ (called coe in lemmas) and from ℝ≥0∞ (coe_ennreal) are registered and their basic properties proved. The latter takes up most of the rest of this file.

Tags

real, ereal, complete lattice

def EReal : Type

The type of extended real numbers [-∞, ∞], constructed as WithBot (WithTop ℝ).

Equations

• EReal = WithBot (WithTop ℝ)

instance instERealBot : Bot EReal

Equations

• instERealBot = WithBot.bot

instance instERealZero : Zero EReal

Equations

• instERealZero = WithBot.zero

instance instERealOne : One EReal

Equations

• instERealOne = WithBot.one

instance instERealNontrivial : Nontrivial EReal

Equations

• instERealNontrivial = ⋯

instance instERealAddMonoid : AddMonoid EReal

Equations

• instERealAddMonoid = WithBot.addMonoid

instance instERealPartialOrder : PartialOrder EReal

Equations

• instERealPartialOrder = WithBot.partialOrder

instance instZeroLEOneClassEReal : ZeroLEOneClass EReal

instance instSupSetEReal : SupSet EReal

Equations

• instSupSetEReal = inferInstanceAs (SupSet (WithBot (WithTop ℝ)))

instance instInfSetEReal : InfSet EReal

Equations

• instInfSetEReal = inferInstanceAs (InfSet (WithBot (WithTop ℝ)))

instance instCompleteLinearOrderEReal : CompleteLinearOrder EReal

Equations

• instCompleteLinearOrderEReal = inferInstanceAs (CompleteLinearOrder (WithBot (WithTop ℝ)))

instance instLinearOrderedAddCommMonoidEReal : LinearOrderedAddCommMonoid EReal

Equations

• instLinearOrderedAddCommMonoidEReal = inferInstanceAs (LinearOrderedAddCommMonoid (WithBot (WithTop ℝ)))

instance instAddCommMonoidWithOneEReal : AddCommMonoidWithOne EReal

Equations

• instAddCommMonoidWithOneEReal = inferInstanceAs (AddCommMonoidWithOne (WithBot (WithTop ℝ)))

instance instDenselyOrderedEReal : DenselyOrdered EReal

instance instCharZeroEReal : CharZero EReal

def Real.toEReal : ℝ → EReal

The canonical inclusion from reals to ereals. Registered as a coercion.

Equations

• Real.toEReal = WithBot.some ∘ WithTop.some

instance EReal.decidableLT : DecidableLT EReal

Equations

• EReal.decidableLT = WithBot.decidableLT

instance EReal.instTop : Top EReal

Equations

• EReal.instTop = { top := ↑⊤ }

instance EReal.instCoeReal : Coe ℝ EReal

Equations

• EReal.instCoeReal = { coe := Real.toEReal }

theorem EReal.coe_strictMono : StrictMono Real.toEReal

theorem EReal.coe_injective : Function.Injective Real.toEReal

@[simp]

theorem EReal.coe_le_coe_iff {x y : ℝ} : ↑x ≤ ↑y ↔ x ≤ y

@[simp]

theorem EReal.coe_lt_coe_iff {x y : ℝ} : ↑x < ↑y ↔ x < y

@[simp]

theorem EReal.coe_eq_coe_iff {x y : ℝ} : ↑x = ↑y ↔ x = y

theorem EReal.coe_ne_coe_iff {x y : ℝ} : ↑x ≠ ↑y ↔ x ≠ y

def ENNReal.toEReal : ENNReal → EReal

The canonical map from nonnegative extended reals to extended reals.

Equations

• ↑none = ⊤
• ↑(some x_1) = ↑↑x_1

instance EReal.hasCoeENNReal : Coe ENNReal EReal

Equations

• EReal.hasCoeENNReal = { coe := ENNReal.toEReal }

instance EReal.instInhabited : Inhabited EReal

Equations

• EReal.instInhabited = { default := 0 }

@[simp]

theorem EReal.coe_zero : ↑0 = 0

@[simp]

theorem EReal.coe_one : ↑1 = 1

def EReal.rec {motive : EReal → Sort u_1} (bot : motive ⊥) (coe : (a : ℝ) → motive ↑a) (top : motive ⊤) (a : EReal) : motive a

A recursor for EReal in terms of the coercion.

When working in term mode, note that pattern matching can be used directly.

Equations

• EReal.rec bot coe top none = bot
• EReal.rec bot coe top (some (some a)) = coe a
• EReal.rec bot coe top (some none) = top

theorem EReal.forall {p : EReal → Prop} : (∀ (r : EReal), p r) ↔ p ⊥ ∧ p ⊤ ∧ ∀ (r : ℝ), p ↑r

theorem EReal.exists {p : EReal → Prop} : (∃ (r : EReal), p r) ↔ p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p ↑r

def EReal.mul : EReal → EReal → EReal

The multiplication on EReal. Our definition satisfies 0 * x = x * 0 = 0 for any x, and picks the only sensible value elsewhere.

Equations

• EReal.mul none none = ⊤
• EReal.mul none (some none) = ⊥
• EReal.mul none (some (some y)) = if 0 < y then ⊥ else if y = 0 then 0 else ⊤
• EReal.mul (some none) none = ⊥
• EReal.mul (some none) (some none) = ⊤
• EReal.mul (some none) (some (some y)) = if 0 < y then ⊤ else if y = 0 then 0 else ⊥
• EReal.mul (some (some x_2)) (some none) = if 0 < x_2 then ⊤ else if x_2 = 0 then 0 else ⊥
• EReal.mul (some (some x_2)) none = if 0 < x_2 then ⊥ else if x_2 = 0 then 0 else ⊤
• EReal.mul (some (some x_2)) (some (some y)) = ↑(x_2 * y)

instance EReal.instMul : Mul EReal

Equations

• EReal.instMul = { mul := EReal.mul }

@[simp]

theorem EReal.coe_mul (x y : ℝ) : ↑(x * y) = ↑x * ↑y

theorem EReal.induction₂ {P : EReal → EReal → Prop} (top_top : P ⊤ ⊤) (top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x) (top_zero : P ⊤ 0) (top_neg : ∀ x < 0, P ⊤ ↑x) (top_bot : P ⊤ ⊥) (pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤) (pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥) (zero_top : P 0 ⊤) (coe_coe : ∀ (x y : ℝ), P ↑x ↑y) (zero_bot : P 0 ⊥) (neg_top : ∀ x < 0, P ↑x ⊤) (neg_bot : ∀ x < 0, P ↑x ⊥) (bot_top : P ⊥ ⊤) (bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x) (bot_zero : P ⊥ 0) (bot_neg : ∀ x < 0, P ⊥ ↑x) (bot_bot : P ⊥ ⊥) (x y : EReal) : P x y

Induct on two EReals by performing case splits on the sign of one whenever the other is infinite.

theorem EReal.induction₂_symm {P : EReal → EReal → Prop} (symm : ∀ {x y : EReal}, P x y → P y x) (top_top : P ⊤ ⊤) (top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x) (top_zero : P ⊤ 0) (top_neg : ∀ x < 0, P ⊤ ↑x) (top_bot : P ⊤ ⊥) (pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥) (coe_coe : ∀ (x y : ℝ), P ↑x ↑y) (zero_bot : P 0 ⊥) (neg_bot : ∀ x < 0, P ↑x ⊥) (bot_bot : P ⊥ ⊥) (x y : EReal) : P x y

Induct on two EReals by performing case splits on the sign of one whenever the other is infinite. This version eliminates some cases by assuming that the relation is symmetric.

theorem EReal.mul_comm (x y : EReal) : x * y = y * x

theorem EReal.one_mul (x : EReal) : 1 * x = x

theorem EReal.zero_mul (x : EReal) : 0 * x = 0

instance EReal.instMulZeroOneClass : MulZeroOneClass EReal

Equations

• EReal.instMulZeroOneClass = MulZeroOneClass.mk EReal.zero_mul EReal.instMulZeroOneClass.proof_2

Real coercion

instance EReal.canLift : CanLift EReal ℝ Real.toEReal fun (r : EReal) => r ≠ ⊤ ∧ r ≠ ⊥

def EReal.toReal : EReal → ℝ

The map from extended reals to reals sending infinities to zero.

Equations

• EReal.toReal none = 0
• EReal.toReal (some none) = 0
• EReal.toReal (some (some x_1)) = x_1

@[simp]

theorem EReal.toReal_top : ⊤.toReal = 0

@[simp]

theorem EReal.toReal_bot : ⊥.toReal = 0

@[simp]

theorem EReal.toReal_zero : toReal 0 = 0

@[simp]

theorem EReal.toReal_one : toReal 1 = 1

@[simp]

theorem EReal.toReal_coe (x : ℝ) : (↑x).toReal = x

@[simp]

theorem EReal.bot_lt_coe (x : ℝ) : ⊥ < ↑x

@[simp]

theorem EReal.coe_ne_bot (x : ℝ) : ↑x ≠ ⊥

@[simp]

theorem EReal.bot_ne_coe (x : ℝ) : ⊥ ≠ ↑x

@[simp]

theorem EReal.coe_lt_top (x : ℝ) : ↑x < ⊤

@[simp]

theorem EReal.coe_ne_top (x : ℝ) : ↑x ≠ ⊤

@[simp]

theorem EReal.top_ne_coe (x : ℝ) : ⊤ ≠ ↑x

@[simp]

theorem EReal.bot_lt_zero : ⊥ < 0

@[simp]

theorem EReal.bot_ne_zero : ⊥ ≠ 0

@[simp]

theorem EReal.zero_ne_bot : 0 ≠ ⊥

@[simp]

theorem EReal.zero_lt_top : 0 < ⊤

@[simp]

theorem EReal.zero_ne_top : 0 ≠ ⊤

@[simp]

theorem EReal.top_ne_zero : ⊤ ≠ 0

theorem EReal.range_coe : Set.range Real.toEReal = {⊥, ⊤}ᶜ

theorem EReal.range_coe_eq_Ioo : Set.range Real.toEReal = Set.Ioo ⊥ ⊤

@[simp]

theorem EReal.coe_add (x y : ℝ) : ↑(x + y) = ↑x + ↑y

theorem EReal.coe_nsmul (n : ℕ) (x : ℝ) : ↑(n • x) = n • ↑x

@[simp]

theorem EReal.coe_eq_zero {x : ℝ} : ↑x = 0 ↔ x = 0

@[simp]

theorem EReal.coe_eq_one {x : ℝ} : ↑x = 1 ↔ x = 1

theorem EReal.coe_ne_zero {x : ℝ} : ↑x ≠ 0 ↔ x ≠ 0

theorem EReal.coe_ne_one {x : ℝ} : ↑x ≠ 1 ↔ x ≠ 1

@[simp]

theorem EReal.coe_nonneg {x : ℝ} : 0 ≤ ↑x ↔ 0 ≤ x

@[simp]

theorem EReal.coe_nonpos {x : ℝ} : ↑x ≤ 0 ↔ x ≤ 0

@[simp]

theorem EReal.coe_pos {x : ℝ} : 0 < ↑x ↔ 0 < x

@[simp]

theorem EReal.coe_neg' {x : ℝ} : ↑x < 0 ↔ x < 0

theorem EReal.toReal_eq_zero_iff {x : EReal} : x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x = ⊥

theorem EReal.toReal_ne_zero_iff {x : EReal} : x.toReal ≠ 0 ↔ x ≠ 0 ∧ x ≠ ⊤ ∧ x ≠ ⊥

theorem EReal.toReal_eq_toReal {x y : EReal} (hx_top : x ≠ ⊤) (hx_bot : x ≠ ⊥) (hy_top : y ≠ ⊤) (hy_bot : y ≠ ⊥) : x.toReal = y.toReal ↔ x = y

theorem EReal.toReal_nonneg {x : EReal} (hx : 0 ≤ x) : 0 ≤ x.toReal

theorem EReal.toReal_nonpos {x : EReal} (hx : x ≤ 0) : x.toReal ≤ 0

theorem EReal.toReal_le_toReal {x y : EReal} (h : x ≤ y) (hx : x ≠ ⊥) (hy : y ≠ ⊤) : x.toReal ≤ y.toReal

theorem EReal.coe_toReal {x : EReal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) : ↑x.toReal = x

theorem EReal.le_coe_toReal {x : EReal} (h : x ≠ ⊤) : x ≤ ↑x.toReal

theorem EReal.coe_toReal_le {x : EReal} (h : x ≠ ⊥) : ↑x.toReal ≤ x

theorem EReal.eq_top_iff_forall_lt (x : EReal) : x = ⊤ ↔ ∀ (y : ℝ), ↑y < x

theorem EReal.eq_bot_iff_forall_lt (x : EReal) : x = ⊥ ↔ ∀ (y : ℝ), x < ↑y

Intervals and coercion from reals

theorem EReal.exists_between_coe_real {x z : EReal} (h : x < z) : ∃ (y : ℝ), x < ↑y ∧ ↑y < z

@[simp]

theorem EReal.image_coe_Icc (x y : ℝ) : Real.toEReal '' Set.Icc x y = Set.Icc ↑x ↑y

@[simp]

theorem EReal.image_coe_Ico (x y : ℝ) : Real.toEReal '' Set.Ico x y = Set.Ico ↑x ↑y

@[simp]

theorem EReal.image_coe_Ici (x : ℝ) : Real.toEReal '' Set.Ici x = Set.Ico ↑x ⊤

@[simp]

theorem EReal.image_coe_Ioc (x y : ℝ) : Real.toEReal '' Set.Ioc x y = Set.Ioc ↑x ↑y

@[simp]

theorem EReal.image_coe_Ioo (x y : ℝ) : Real.toEReal '' Set.Ioo x y = Set.Ioo ↑x ↑y

@[simp]

theorem EReal.image_coe_Ioi (x : ℝ) : Real.toEReal '' Set.Ioi x = Set.Ioo ↑x ⊤

@[simp]

theorem EReal.image_coe_Iic (x : ℝ) : Real.toEReal '' Set.Iic x = Set.Ioc ⊥ ↑x

@[simp]

theorem EReal.image_coe_Iio (x : ℝ) : Real.toEReal '' Set.Iio x = Set.Ioo ⊥ ↑x

@[simp]

theorem EReal.preimage_coe_Ici (x : ℝ) : Real.toEReal ⁻¹' Set.Ici ↑x = Set.Ici x

@[simp]

theorem EReal.preimage_coe_Ioi (x : ℝ) : Real.toEReal ⁻¹' Set.Ioi ↑x = Set.Ioi x

@[simp]

theorem EReal.preimage_coe_Ioi_bot : Real.toEReal ⁻¹' Set.Ioi ⊥ = Set.univ

@[simp]

theorem EReal.preimage_coe_Iic (y : ℝ) : Real.toEReal ⁻¹' Set.Iic ↑y = Set.Iic y

@[simp]

theorem EReal.preimage_coe_Iio (y : ℝ) : Real.toEReal ⁻¹' Set.Iio ↑y = Set.Iio y

@[simp]

theorem EReal.preimage_coe_Iio_top : Real.toEReal ⁻¹' Set.Iio ⊤ = Set.univ

@[simp]

theorem EReal.preimage_coe_Icc (x y : ℝ) : Real.toEReal ⁻¹' Set.Icc ↑x ↑y = Set.Icc x y

@[simp]

theorem EReal.preimage_coe_Ico (x y : ℝ) : Real.toEReal ⁻¹' Set.Ico ↑x ↑y = Set.Ico x y

@[simp]

theorem EReal.preimage_coe_Ioc (x y : ℝ) : Real.toEReal ⁻¹' Set.Ioc ↑x ↑y = Set.Ioc x y

@[simp]

theorem EReal.preimage_coe_Ioo (x y : ℝ) : Real.toEReal ⁻¹' Set.Ioo ↑x ↑y = Set.Ioo x y

@[simp]

theorem EReal.preimage_coe_Ico_top (x : ℝ) : Real.toEReal ⁻¹' Set.Ico ↑x ⊤ = Set.Ici x

@[simp]

theorem EReal.preimage_coe_Ioo_top (x : ℝ) : Real.toEReal ⁻¹' Set.Ioo ↑x ⊤ = Set.Ioi x

@[simp]

theorem EReal.preimage_coe_Ioc_bot (y : ℝ) : Real.toEReal ⁻¹' Set.Ioc ⊥ ↑y = Set.Iic y

@[simp]

theorem EReal.preimage_coe_Ioo_bot (y : ℝ) : Real.toEReal ⁻¹' Set.Ioo ⊥ ↑y = Set.Iio y

@[simp]

theorem EReal.preimage_coe_Ioo_bot_top : Real.toEReal ⁻¹' Set.Ioo ⊥ ⊤ = Set.univ

ennreal coercion

@[simp]

theorem EReal.toReal_coe_ennreal {x : ENNReal} : (↑x).toReal = x.toReal

@[simp]

theorem EReal.coe_ennreal_ofReal {x : ℝ} : ↑(ENNReal.ofReal x) = ↑(x ⊔ 0)

theorem EReal.coe_ennreal_toReal {x : ENNReal} (hx : x ≠ ⊤) : ↑x.toReal = ↑x

theorem EReal.coe_nnreal_eq_coe_real (x : NNReal) : ↑↑x = ↑↑x

@[simp]

theorem EReal.coe_ennreal_zero : ↑0 = 0

@[simp]

theorem EReal.coe_ennreal_one : ↑1 = 1

@[simp]

theorem EReal.coe_ennreal_top : ↑⊤ = ⊤

theorem EReal.coe_ennreal_strictMono : StrictMono ENNReal.toEReal

theorem EReal.coe_ennreal_injective : Function.Injective ENNReal.toEReal

@[simp]

theorem EReal.coe_ennreal_eq_top_iff {x : ENNReal} : ↑x = ⊤ ↔ x = ⊤

theorem EReal.coe_nnreal_ne_top (x : NNReal) : ↑↑x ≠ ⊤

@[simp]

theorem EReal.coe_nnreal_lt_top (x : NNReal) : ↑↑x < ⊤

@[simp]

theorem EReal.coe_ennreal_le_coe_ennreal_iff {x y : ENNReal} : ↑x ≤ ↑y ↔ x ≤ y

@[simp]

theorem EReal.coe_ennreal_lt_coe_ennreal_iff {x y : ENNReal} : ↑x < ↑y ↔ x < y

@[simp]

theorem EReal.coe_ennreal_eq_coe_ennreal_iff {x y : ENNReal} : ↑x = ↑y ↔ x = y

theorem EReal.coe_ennreal_ne_coe_ennreal_iff {x y : ENNReal} : ↑x ≠ ↑y ↔ x ≠ y

@[simp]

theorem EReal.coe_ennreal_eq_zero {x : ENNReal} : ↑x = 0 ↔ x = 0

@[simp]

theorem EReal.coe_ennreal_eq_one {x : ENNReal} : ↑x = 1 ↔ x = 1

theorem EReal.coe_ennreal_ne_zero {x : ENNReal} : ↑x ≠ 0 ↔ x ≠ 0

theorem EReal.coe_ennreal_ne_one {x : ENNReal} : ↑x ≠ 1 ↔ x ≠ 1

theorem EReal.coe_ennreal_nonneg (x : ENNReal) : 0 ≤ ↑x

@[simp]

theorem EReal.range_coe_ennreal : Set.range ENNReal.toEReal = Set.Ici 0

instance EReal.instCanLiftENNRealToERealLeOfNat : CanLift EReal ENNReal ENNReal.toEReal fun (x : EReal) => 0 ≤ x

@[simp]

theorem EReal.coe_ennreal_pos {x : ENNReal} : 0 < ↑x ↔ 0 < x

@[simp]

theorem EReal.bot_lt_coe_ennreal (x : ENNReal) : ⊥ < ↑x

@[simp]

theorem EReal.coe_ennreal_ne_bot (x : ENNReal) : ↑x ≠ ⊥

@[simp]

theorem EReal.coe_ennreal_add (x y : ENNReal) : ↑(x + y) = ↑x + ↑y

@[simp]

theorem EReal.coe_ennreal_mul (x y : ENNReal) : ↑(x * y) = ↑x * ↑y

theorem EReal.coe_ennreal_nsmul (n : ℕ) (x : ENNReal) : ↑(n • x) = n • ↑x

toENNReal

noncomputable def EReal.toENNReal (x : EReal) : ENNReal

x.toENNReal returns x if it is nonnegative, 0 otherwise.

Equations

• x.toENNReal = if x = ⊤ then ⊤ else ENNReal.ofReal x.toReal

@[simp]

theorem EReal.toENNReal_top : ⊤.toENNReal = ⊤

@[simp]

theorem EReal.toENNReal_of_ne_top {x : EReal} (hx : x ≠ ⊤) : x.toENNReal = ENNReal.ofReal x.toReal

@[simp]

theorem EReal.toENNReal_eq_top_iff {x : EReal} : x.toENNReal = ⊤ ↔ x = ⊤

theorem EReal.toENNReal_ne_top_iff {x : EReal} : x.toENNReal ≠ ⊤ ↔ x ≠ ⊤

@[simp]

theorem EReal.toENNReal_of_nonpos {x : EReal} (hx : x ≤ 0) : x.toENNReal = 0

theorem EReal.toENNReal_bot : ⊥.toENNReal = 0

theorem EReal.toENNReal_zero : toENNReal 0 = 0

theorem EReal.toENNReal_eq_zero_iff {x : EReal} : x.toENNReal = 0 ↔ x ≤ 0

theorem EReal.toENNReal_ne_zero_iff {x : EReal} : x.toENNReal ≠ 0 ↔ 0 < x

@[simp]

theorem EReal.coe_toENNReal {x : EReal} (hx : 0 ≤ x) : ↑x.toENNReal = x

theorem EReal.coe_toENNReal_eq_max {x : EReal} : ↑x.toENNReal = 0 ⊔ x

@[simp]

theorem EReal.toENNReal_coe {x : ENNReal} : (↑x).toENNReal = x

@[simp]

theorem EReal.real_coe_toENNReal (x : ℝ) : (↑x).toENNReal = ENNReal.ofReal x

@[simp]

theorem EReal.toReal_toENNReal {x : EReal} (hx : 0 ≤ x) : x.toENNReal.toReal = x.toReal

theorem EReal.toENNReal_eq_toENNReal {x y : EReal} (hx : 0 ≤ x) (hy : 0 ≤ y) : x.toENNReal = y.toENNReal ↔ x = y

theorem EReal.toENNReal_le_toENNReal {x y : EReal} (h : x ≤ y) : x.toENNReal ≤ y.toENNReal

theorem EReal.toENNReal_lt_toENNReal {x y : EReal} (hx : 0 ≤ x) (hxy : x < y) : x.toENNReal < y.toENNReal

nat coercion

theorem EReal.coe_coe_eq_natCast (n : ℕ) : ↑↑n = ↑n

theorem EReal.natCast_ne_bot (n : ℕ) : ↑n ≠ ⊥

theorem EReal.natCast_ne_top (n : ℕ) : ↑n ≠ ⊤

theorem EReal.natCast_eq_iff {m n : ℕ} : ↑m = ↑n ↔ m = n

theorem EReal.natCast_ne_iff {m n : ℕ} : ↑m ≠ ↑n ↔ m ≠ n

theorem EReal.natCast_le_iff {m n : ℕ} : ↑m ≤ ↑n ↔ m ≤ n

theorem EReal.natCast_lt_iff {m n : ℕ} : ↑m < ↑n ↔ m < n

@[simp]

theorem EReal.natCast_mul (m n : ℕ) : ↑(m * n) = ↑m * ↑n

Miscellaneous lemmas

theorem EReal.exists_rat_btwn_of_lt {a b : EReal} : a < b → ∃ (x : ℚ), a < ↑↑x ∧ ↑↑x < b

theorem EReal.lt_iff_exists_rat_btwn {a b : EReal} : a < b ↔ ∃ (x : ℚ), a < ↑↑x ∧ ↑↑x < b

theorem EReal.lt_iff_exists_real_btwn {a b : EReal} : a < b ↔ ∃ (x : ℝ), a < ↑x ∧ ↑x < b

def EReal.neTopBotEquivReal : ↑{⊥, ⊤}ᶜ ≃ ℝ

The set of numbers in EReal that are not equal to ±∞ is equivalent to ℝ.

Equations

• One or more equations did not get rendered due to their size.