Documentation

Mathlib.Data.EReal.Basic

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 :

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

Instances For

@[implicit_reducible]

noncomputable instance instNontrivialEReal :

Nontrivial EReal

@[implicit_reducible]

noncomputable instance instZeroEReal :

Zero EReal

@[implicit_reducible]

noncomputable instance instOneEReal :

@[implicit_reducible]

noncomputable instance instAddMonoidEReal :

AddMonoid EReal

@[implicit_reducible]

noncomputable instance instAddCommMonoidEReal :

AddCommMonoid EReal

@[implicit_reducible]

noncomputable instance instAddCommMonoidWithOneEReal :

AddCommMonoidWithOne EReal

@[implicit_reducible]

noncomputable instance instCharZeroEReal :

@[implicit_reducible]

noncomputable instance instTopEReal :

@[implicit_reducible]

noncomputable instance instBotEReal :

@[implicit_reducible]

noncomputable instance instSupSetEReal :

@[implicit_reducible]

noncomputable instance instInfSetEReal :

@[implicit_reducible]

noncomputable instance instPartialOrderEReal :

PartialOrder EReal

@[implicit_reducible]

noncomputable instance instLinearOrderEReal :

LinearOrder EReal

@[implicit_reducible]

noncomputable instance instCompleteLinearOrderEReal :

CompleteLinearOrder EReal

@[implicit_reducible]

noncomputable instance instDenselyOrderedEReal :

DenselyOrdered EReal

@[implicit_reducible]

noncomputable instance instZeroLEOneClassEReal :

ZeroLEOneClass EReal

@[implicit_reducible]

noncomputable instance instIsOrderedAddMonoidEReal :

IsOrderedAddMonoid EReal

def Real.toEReal :

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

Instances For

@[implicit_reducible]

instance EReal.instCoeReal :

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

theorem EReal.coe_le_coe {x y : ℝ} :

x ≤ y → ↑x ≤ ↑y

Alias of the reverse direction of EReal.coe_le_coe_iff.

@[simp]

theorem EReal.coe_lt_coe_iff {x y : ℝ} :

↑x < ↑y ↔ x < y

theorem EReal.coe_lt_coe {x y : ℝ} :

x < y → ↑x < ↑y

Alias of the reverse direction of EReal.coe_lt_coe_iff.

@[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

@[simp]

theorem EReal.coe_natCast {n : ℕ} :

↑↑n = ↑n

noncomputable def ENNReal.toEReal :

ENNReal → EReal

The canonical map from nonnegative extended reals to extended reals.

Instances For

@[implicit_reducible]

noncomputable instance EReal.hasCoeENNReal :

Coe ENNReal EReal

@[implicit_reducible]

noncomputable instance EReal.instInhabited :

Inhabited EReal

@[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, although this is prone to leaking the implementation details in terms of Option.

Instances For

@[simp]

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

EReal.rec bot coe top ⊥ = bot

@[simp]

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

EReal.rec bot coe top ⊤ = top

@[simp]

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

EReal.rec bot coe top ↑a = coe a

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

noncomputable 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.

Instances For

@[implicit_reducible]

noncomputable instance EReal.instMul :

@[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

@[implicit_reducible]

noncomputable instance EReal.instMulZeroOneClass :

MulZeroOneClass EReal

Real coercion #

instance EReal.canLift :

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

def EReal.toReal :

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

Instances For

@[simp]

theorem EReal.toReal_top :

@[simp]

theorem EReal.toReal_bot :

@[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 :

@[simp]

theorem EReal.bot_ne_zero :

⊥ ≠ 0

@[simp]

theorem EReal.zero_ne_bot :

0 ≠ ⊥

@[simp]

theorem EReal.zero_lt_top :

@[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) :

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

theorem EReal.toReal_pos {x : EReal} (hx : 0 < x) (h'x : x ≠ ⊤) :

theorem EReal.toReal_neg {x : EReal} (hx : x < 0) (h'x : x ≠ ⊥) :

@[simp]

theorem EReal.toReal_image_Ioo_zero_top :

toReal '' Set.Ioo 0 ⊤ = Set.Ioi 0

@[simp]

theorem EReal.toReal_image_Ioo_bot_zero :

toReal '' Set.Ioo ⊥ 0 = Set.Iio 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) = ↑(max 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

theorem EReal.coe_ennreal_pos_iff_ne_zero {x : ENNReal} :

0 < ↑x ↔ x ≠ 0

@[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) :

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

Instances For

@[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.toENNReal_pos_iff {x : EReal} :

0 < x.toENNReal ↔ 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 = max 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 ℝ.

Instances For

def Mathlib.Meta.Positivity.evalRealToEReal :

Extension for the positivity tactic: cast from ℝ to EReal.

Instances For

def Mathlib.Meta.Positivity.evalENNRealToEReal :

Extension for the positivity tactic: cast from ℝ≥0∞ to EReal.

Instances For

def Mathlib.Meta.Positivity.evalERealToReal :

Extension for the positivity tactic: projection from EReal to ℝ.

We prove that EReal.toReal x is nonnegative whenever x is nonnegative. Since EReal.toReal ⊤ = 0, we cannot prove a stronger statement, at least without relying on a tactic like finiteness.

Instances For

def Mathlib.Meta.Positivity.evalERealToENNReal :

Extension for the positivity tactic: projection from EReal to ℝ≥0∞.

We show that EReal.toENNReal x is positive whenever x is positive, and it is nonnegative otherwise. We cannot deduce any corollaries from x ≠ 0, since EReal.toENNReal x = 0 for x < 0.

Instances For