mathlib documentation

data.real.ennreal

Extended non-negative reals

We define ennreal := with_no ℝ≥0 to be the type of extended nonnegative real numbers, i.e., the interval [0, +∞]. This type is used as the codomain of a measure_theory.measure, and of the extended distance edist in a emetric_space. In this file we define some algebraic operations and a linear order on ennreal and prove basic properties of these operations, order, and conversions to/from , ℝ≥0, and .

Main definitions

Implementation notes

We define a can_lift ennreal ℝ≥0 instance, so one of the ways to prove theorems about an ennreal number a is to consider the cases a = ∞ and a ≠ ∞, and use the tactic lift a to ℝ≥0 using ha in the second case. This instance is even more useful if one already has ha : a ≠ ∞ in the context, or if we have (f : α → ennreal) (hf : ∀ x, f x ≠ ⊤).

Notations

def ennreal  :
Type

The extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.

Equations
@[instance]

Equations
@[instance]

Equations
@[simp]

@[simp]
theorem ennreal.some_eq_coe (a : ℝ≥0) :

to_nnreal x returns x if it is real, otherwise 0.

Equations

to_real x returns x if it is real, 0 otherwise.

Equations

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

Equations
@[simp]

@[simp]
theorem ennreal.coe_to_nnreal {a : ennreal} :
a (a.to_nnreal) = a

@[simp]

@[simp]
theorem ennreal.to_real_of_real {r : } :

theorem ennreal.of_real_eq_coe_nnreal {x : } (h : 0 x) :

@[simp]
theorem ennreal.coe_zero  :
0 = 0

@[simp]
theorem ennreal.coe_one  :
1 = 1

@[simp]
theorem ennreal.to_real_nonneg {a : ennreal} :

@[simp]

@[simp]

@[simp]
theorem ennreal.one_to_real  :

@[simp]

@[simp]

@[simp]

@[simp]
theorem ennreal.zero_to_real  :

@[simp]

@[simp]

theorem ennreal.forall_ennreal {p : ennreal → Prop} :
(∀ (a : ennreal), p a) (∀ (r : ℝ≥0), p r) p

theorem ennreal.forall_ne_top {p : ennreal → Prop} :
(∀ (a : ennreal), a p a) ∀ (r : ℝ≥0), p r

theorem ennreal.exists_ne_top {p : ennreal → Prop} :
(∃ (a : ennreal) (H : a ), p a) ∃ (r : ℝ≥0), p r

@[simp]
theorem ennreal.coe_ne_top {r : ℝ≥0} :

@[simp]
theorem ennreal.top_ne_coe {r : ℝ≥0} :

@[simp]

@[simp]
theorem ennreal.zero_ne_top  :

@[simp]
theorem ennreal.top_ne_zero  :

@[simp]
theorem ennreal.one_ne_top  :

@[simp]
theorem ennreal.top_ne_one  :

@[simp]
theorem ennreal.coe_eq_coe {r q : ℝ≥0} :
r = q r = q

@[simp]
theorem ennreal.coe_le_coe {r q : ℝ≥0} :
r q r q

@[simp]
theorem ennreal.coe_lt_coe {r q : ℝ≥0} :
r < q r < q

@[simp]
theorem ennreal.coe_eq_zero {r : ℝ≥0} :
r = 0 r = 0

@[simp]
theorem ennreal.zero_eq_coe {r : ℝ≥0} :
0 = r 0 = r

@[simp]
theorem ennreal.coe_eq_one {r : ℝ≥0} :
r = 1 r = 1

@[simp]
theorem ennreal.one_eq_coe {r : ℝ≥0} :
1 = r 1 = r

@[simp]
theorem ennreal.coe_nonneg {r : ℝ≥0} :
0 r 0 r

@[simp]
theorem ennreal.coe_pos {r : ℝ≥0} :
0 < r 0 < r

@[simp]
theorem ennreal.coe_add {r p : ℝ≥0} :
(r + p) = r + p

@[simp]
theorem ennreal.coe_mul {r p : ℝ≥0} :
r * p = (r) * p

@[simp]
theorem ennreal.coe_bit0 {r : ℝ≥0} :

@[simp]
theorem ennreal.coe_bit1 {r : ℝ≥0} :

theorem ennreal.coe_two  :
2 = 2

theorem ennreal.zero_lt_one  :
0 < 1

@[simp]
theorem ennreal.one_lt_two  :
1 < 2

@[simp]
theorem ennreal.zero_lt_two  :
0 < 2

theorem ennreal.two_ne_zero  :
2 0

The set of ennreal numbers that are not equal to is equivalent to ℝ≥0.

Equations
theorem ennreal.cinfi_ne_top {α : Type u_1} [has_Inf α] (f : ennreal → α) :
(⨅ (x : {x // x }), f x) = ⨅ (x : ℝ≥0), f x

theorem ennreal.infi_ne_top {α : Type u_1} [complete_lattice α] (f : ennreal → α) :
(⨅ (x : ennreal) (H : x ), f x) = ⨅ (x : ℝ≥0), f x

theorem ennreal.csupr_ne_top {α : Type u_1} [has_Sup α] (f : ennreal → α) :
(⨆ (x : {x // x }), f x) = ⨆ (x : ℝ≥0), f x

theorem ennreal.supr_ne_top {α : Type u_1} [complete_lattice α] (f : ennreal → α) :
(⨆ (x : ennreal) (H : x ), f x) = ⨆ (x : ℝ≥0), f x

theorem ennreal.infi_ennreal {α : Type u_1} [complete_lattice α] {f : ennreal → α} :
(⨅ (n : ennreal), f n) = (⨅ (n : ℝ≥0), f n) f

theorem ennreal.supr_ennreal {α : Type u_1} [complete_lattice α] {f : ennreal → α} :
(⨆ (n : ennreal), f n) = (⨆ (n : ℝ≥0), f n) f

@[simp]
theorem ennreal.add_top {a : ennreal} :

@[simp]
theorem ennreal.top_add {a : ennreal} :

Coercion ℝ≥0 → ennreal as a ring_hom.

Equations
@[simp]
theorem ennreal.coe_indicator {α : Type u_1} (s : set α) (f : α → ℝ≥0) (a : α) :
(s.indicator f a) = s.indicator (λ (x : α), (f x)) a

@[simp]
theorem ennreal.coe_pow {r : ℝ≥0} (n : ) :
(r ^ n) = r ^ n

theorem ennreal.add_eq_top {a b : ennreal} :
a + b = a = b =

theorem ennreal.add_lt_top {a b : ennreal} :
a + b < a < b <

theorem ennreal.to_nnreal_add {r₁ r₂ : ennreal} :
r₁ < r₂ < (r₁ + r₂).to_nnreal = r₁.to_nnreal + r₂.to_nnreal

theorem ennreal.bot_lt_iff_ne_bot {a : ennreal} :
0 < a a 0

theorem ennreal.not_lt_top {x : ennreal} :

theorem ennreal.add_ne_top {a b : ennreal} :

theorem ennreal.mul_top {a : ennreal} :
a * = ite (a = 0) 0

theorem ennreal.top_mul {a : ennreal} :
* a = ite (a = 0) 0

@[simp]

theorem ennreal.top_pow {n : } :
0 < n ^ n =

theorem ennreal.mul_eq_top {a b : ennreal} :
a * b = a 0 b = a = b 0

theorem ennreal.mul_ne_top {a b : ennreal} :
a b a * b

theorem ennreal.mul_lt_top {a b : ennreal} :
a < b < a * b <

theorem ennreal.ne_top_of_mul_ne_top_left {a b : ennreal} :
a * b b 0a

theorem ennreal.ne_top_of_mul_ne_top_right {a b : ennreal} :
a * b a 0b

theorem ennreal.lt_top_of_mul_lt_top_left {a b : ennreal} :
a * b < b 0a <

theorem ennreal.lt_top_of_mul_lt_top_right {a b : ennreal} :
a * b < a 0b <

theorem ennreal.mul_lt_top_iff {a b : ennreal} :
a * b < a < b < a = 0 b = 0

@[simp]
theorem ennreal.mul_pos {a b : ennreal} :
0 < a * b 0 < a 0 < b

theorem ennreal.pow_eq_top {a : ennreal} (n : ) :
a ^ n = a =

theorem ennreal.pow_ne_top {a : ennreal} (h : a ) {n : } :
a ^ n

theorem ennreal.pow_lt_top {a : ennreal} (a_1 : a < ) (n : ) :
a ^ n <

@[simp]
theorem ennreal.coe_finset_sum {α : Type u_1} {s : finset α} {f : α → ℝ≥0} :
∑ (a : α) in s, f a = ∑ (a : α) in s, (f a)

@[simp]
theorem ennreal.coe_finset_prod {α : Type u_1} {s : finset α} {f : α → ℝ≥0} :
∏ (a : α) in s, f a = ∏ (a : α) in s, (f a)

@[simp]
theorem ennreal.bot_eq_zero  :
= 0

@[simp]
theorem ennreal.coe_lt_top {r : ℝ≥0} :

@[simp]

theorem ennreal.zero_lt_coe_iff {p : ℝ≥0} :
0 < p 0 < p

@[simp]
theorem ennreal.one_le_coe_iff {r : ℝ≥0} :
1 r 1 r

@[simp]
theorem ennreal.coe_le_one_iff {r : ℝ≥0} :
r 1 r 1

@[simp]
theorem ennreal.coe_lt_one_iff {p : ℝ≥0} :
p < 1 p < 1

@[simp]
theorem ennreal.one_lt_coe_iff {p : ℝ≥0} :
1 < p 1 < p

@[simp]
theorem ennreal.coe_nat (n : ) :

@[simp]
theorem ennreal.nat_ne_top (n : ) :

@[simp]
theorem ennreal.top_ne_nat (n : ) :

@[simp]
theorem ennreal.one_lt_top  :
1 <

theorem ennreal.le_coe_iff {a : ennreal} {r : ℝ≥0} :
a r ∃ (p : ℝ≥0), a = p p r

theorem ennreal.coe_le_iff {a : ennreal} {r : ℝ≥0} :
r a ∀ (p : ℝ≥0), a = pr p

theorem ennreal.lt_iff_exists_coe {a b : ennreal} :
a < b ∃ (p : ℝ≥0), a = p p < b

theorem ennreal.pow_le_pow {a : ennreal} {n m : } :
1 an ma ^ n a ^ m

@[simp]
theorem ennreal.max_eq_zero_iff {a b : ennreal} :
max a b = 0 a = 0 b = 0

@[simp]
theorem ennreal.max_zero_left {a : ennreal} :
max 0 a = a

@[simp]
theorem ennreal.max_zero_right {a : ennreal} :
max a 0 = a

@[simp]
theorem ennreal.sup_eq_max {a b : ennreal} :
a b = max a b

theorem ennreal.pow_pos {a : ennreal} (a_1 : 0 < a) (n : ) :
0 < a ^ n

theorem ennreal.pow_ne_zero {a : ennreal} (a_1 : a 0) (n : ) :
a ^ n 0

@[simp]
theorem ennreal.not_lt_zero {a : ennreal} :
¬a < 0

theorem ennreal.add_lt_add_iff_left {a b c : ennreal} :
a < (a + c < a + b c < b)

theorem ennreal.add_lt_add_iff_right {a b c : ennreal} :
a < (c + a < b + a c < b)

theorem ennreal.lt_add_right {a b : ennreal} :
a < 0 < ba < a + b

theorem ennreal.le_of_forall_epsilon_le {a b : ennreal} :
(∀ (ε : ℝ≥0), 0 < εb < a b + ε)a b

theorem ennreal.lt_iff_exists_nnreal_btwn {a b : ennreal} :
a < b ∃ (r : ℝ≥0), a < r r < b

theorem ennreal.lt_iff_exists_add_pos_lt {a b : ennreal} :
a < b ∃ (r : ℝ≥0), 0 < r a + r < b

theorem ennreal.coe_nat_lt_coe {r : ℝ≥0} {n : } :
n < r n < r

theorem ennreal.coe_lt_coe_nat {r : ℝ≥0} {n : } :
r < n r < n

theorem ennreal.coe_nat_lt_coe_nat {m n : } :
m < n m < n

theorem ennreal.coe_nat_le_coe_nat {m n : } :
m n m n

theorem ennreal.exists_nat_gt {r : ennreal} :
r (∃ (n : ), r < n)

theorem ennreal.add_lt_add {a b c d : ennreal} :
a < cb < da + b < c + d

theorem ennreal.coe_min {r p : ℝ≥0} :
(min r p) = min r p

theorem ennreal.coe_max {r p : ℝ≥0} :
(max r p) = max r p

theorem ennreal.coe_Sup {s : set ℝ≥0} :
bdd_above s((Sup s) = ⨆ (a : ℝ≥0) (H : a s), a)

theorem ennreal.coe_Inf {s : set ℝ≥0} :
s.nonempty((Inf s) = ⨅ (a : ℝ≥0) (H : a s), a)

theorem ennreal.mul_le_mul {a b c d : ennreal} :
a bc da * c b * d

theorem ennreal.mul_right_mono {a : ennreal} :
monotone (λ (x : ennreal), x * a)

theorem ennreal.max_mul {a b c : ennreal} :
(max a b) * c = max (a * c) (b * c)

theorem ennreal.mul_max {a b c : ennreal} :
a * max b c = max (a * b) (a * c)

theorem ennreal.mul_eq_mul_left {a b c : ennreal} :
a 0a (a * b = a * c b = c)

theorem ennreal.mul_eq_mul_right {a b c : ennreal} :
c 0c (a * c = b * c a = b)

theorem ennreal.mul_le_mul_left {a b c : ennreal} :
a 0a (a * b a * c b c)

theorem ennreal.mul_le_mul_right {a b c : ennreal} :
c 0c (a * c b * c a b)

theorem ennreal.mul_lt_mul_left {a b c : ennreal} :
a 0a (a * b < a * c b < c)

theorem ennreal.mul_lt_mul_right {a b c : ennreal} :
c 0c (a * c < b * c a < b)

@[instance]

Equations
theorem ennreal.coe_sub {r p : ℝ≥0} :
(p - r) = p - r

@[simp]
theorem ennreal.top_sub_coe {r : ℝ≥0} :

@[simp]
theorem ennreal.sub_eq_zero_of_le {a b : ennreal} :
a ba - b = 0

@[simp]
theorem ennreal.sub_self {a : ennreal} :
a - a = 0

@[simp]
theorem ennreal.zero_sub {a : ennreal} :
0 - a = 0

@[simp]
theorem ennreal.sub_infty {a : ennreal} :
a - = 0

theorem ennreal.sub_le_sub {a b c d : ennreal} :
a bd ca - c b - d

@[simp]
theorem ennreal.add_sub_self {a b : ennreal} :
b < a + b - b = a

@[simp]
theorem ennreal.add_sub_self' {a b : ennreal} :
a < a + b - a = b

theorem ennreal.add_right_inj {a b c : ennreal} :
a < (a + b = a + c b = c)

theorem ennreal.add_left_inj {a b c : ennreal} :
a < (b + a = c + a b = c)

@[simp]
theorem ennreal.sub_add_cancel_of_le {a b : ennreal} :
b aa - b + b = a

@[simp]
theorem ennreal.add_sub_cancel_of_le {a b : ennreal} :
b ab + (a - b) = a

theorem ennreal.sub_add_self_eq_max {a b : ennreal} :
a - b + b = max a b

theorem ennreal.le_sub_add_self {a b : ennreal} :
a a - b + b

@[simp]
theorem ennreal.sub_le_iff_le_add {a b c : ennreal} :
a - b c a c + b

theorem ennreal.sub_le_iff_le_add' {a b c : ennreal} :
a - b c a b + c

theorem ennreal.sub_eq_of_add_eq {a b c : ennreal} :
b a + b = cc - b = a

theorem ennreal.sub_le_of_sub_le {a b c : ennreal} :
a - b ca - c b

theorem ennreal.sub_lt_sub_self {a b : ennreal} :
a a 00 < ba - b < a

@[simp]
theorem ennreal.sub_eq_zero_iff_le {a b : ennreal} :
a - b = 0 a b

@[simp]
theorem ennreal.zero_lt_sub_iff_lt {a b : ennreal} :
0 < a - b b < a

theorem ennreal.lt_sub_iff_add_lt {a b c : ennreal} :
a < b - c a + c < b

theorem ennreal.sub_le_self (a b : ennreal) :
a - b a

@[simp]
theorem ennreal.sub_zero {a : ennreal} :
a - 0 = a

theorem ennreal.sub_le_sub_add_sub {a b c : ennreal} :
a - c a - b + (b - c)

A version of triangle inequality for difference as a "distance".

theorem ennreal.sub_sub_cancel {a b : ennreal} :
a < b aa - (a - b) = b

theorem ennreal.sub_right_inj {a b c : ennreal} :
a < b ac a(a - b = a - c b = c)

theorem ennreal.sub_mul {a b c : ennreal} :
(0 < bb < ac )(a - b) * c = a * c - b * c

theorem ennreal.mul_sub {a b c : ennreal} :
(0 < cc < ba )a * (b - c) = a * b - a * c

theorem ennreal.sub_mul_ge {a b c : ennreal} :
a * c - b * c (a - b) * c

theorem ennreal.sum_lt_top {α : Type u_1} {s : finset α} {f : α → ennreal} :
(∀ (a : α), a sf a < )∑ (a : α) in s, f a <

A sum of finite numbers is still finite

theorem ennreal.sum_lt_top_iff {α : Type u_1} {s : finset α} {f : α → ennreal} :
∑ (a : α) in s, f a < ∀ (a : α), a sf a <

A sum of finite numbers is still finite

theorem ennreal.sum_eq_top_iff {α : Type u_1} {s : finset α} {f : α → ennreal} :
∑ (x : α) in s, f x = ∃ (a : α) (H : a s), f a =

A sum of numbers is infinite iff one of them is infinite

theorem ennreal.to_nnreal_sum {α : Type u_1} {s : finset α} {f : α → ennreal} :
(∀ (a : α), a sf a < )(∑ (a : α) in s, f a).to_nnreal = ∑ (a : α) in s, (f a).to_nnreal

seeing ennreal as nnreal does not change their sum, unless one of the ennreal is infinity

theorem ennreal.to_real_sum {α : Type u_1} {s : finset α} {f : α → ennreal} :
(∀ (a : α), a sf a < )(∑ (a : α) in s, f a).to_real = ∑ (a : α) in s, (f a).to_real

seeing ennreal as real does not change their sum, unless one of the ennreal is infinity

theorem ennreal.mem_Iio_self_add {x ε : ennreal} :
x 0 < εx set.Iio (x + ε)

theorem ennreal.not_mem_Ioo_self_sub {x y ε : ennreal} :
x = 0x set.Ioo (x - ε) y

theorem ennreal.mem_Ioo_self_sub_add {x ε₁ ε₂ : ennreal} :
x x 00 < ε₁0 < ε₂x set.Ioo (x - ε₁) (x + ε₂)

@[simp]
theorem ennreal.bit0_inj {a b : ennreal} :
bit0 a = bit0 b a = b

@[simp]
theorem ennreal.bit0_eq_zero_iff {a : ennreal} :
bit0 a = 0 a = 0

@[simp]
theorem ennreal.bit0_eq_top_iff {a : ennreal} :

@[simp]
theorem ennreal.bit1_inj {a b : ennreal} :
bit1 a = bit1 b a = b

@[simp]
theorem ennreal.bit1_ne_zero {a : ennreal} :
bit1 a 0

@[simp]
theorem ennreal.bit1_eq_one_iff {a : ennreal} :
bit1 a = 1 a = 0

@[simp]
theorem ennreal.bit1_eq_top_iff {a : ennreal} :

@[instance]

Equations
@[instance]

Equations
theorem ennreal.div_def {a b : ennreal} :
a / b = a * b⁻¹

theorem ennreal.mul_div_assoc {a b c : ennreal} :
a * b / c = a * (b / c)

@[simp]
theorem ennreal.inv_zero  :

@[simp]
theorem ennreal.inv_top  :

@[simp]
theorem ennreal.coe_inv {r : ℝ≥0} :
r 0r⁻¹ = (r)⁻¹

@[simp]
theorem ennreal.coe_div {r p : ℝ≥0} :
r 0(p / r) = p / r

@[simp]
theorem ennreal.inv_one  :
1⁻¹ = 1

@[simp]
theorem ennreal.div_one {a : ennreal} :
a / 1 = a

theorem ennreal.inv_pow {a : ennreal} {n : } :
(a ^ n)⁻¹ = a⁻¹ ^ n

@[simp]
theorem ennreal.inv_inv {a : ennreal} :

@[simp]
theorem ennreal.inv_eq_inv {a b : ennreal} :
a⁻¹ = b⁻¹ a = b

@[simp]
theorem ennreal.inv_eq_top {a : ennreal} :
a⁻¹ = a = 0

@[simp]
theorem ennreal.inv_lt_top {x : ennreal} :
x⁻¹ < 0 < x

theorem ennreal.div_lt_top {x y : ennreal} :
x < 0 < yx / y <

@[simp]
theorem ennreal.inv_eq_zero {a : ennreal} :
a⁻¹ = 0 a =

@[simp]
theorem ennreal.inv_pos {a : ennreal} :

@[simp]
theorem ennreal.inv_lt_inv {a b : ennreal} :
a⁻¹ < b⁻¹ b < a

@[simp]
theorem ennreal.inv_le_inv {a b : ennreal} :

@[simp]
theorem ennreal.inv_lt_one {a : ennreal} :
a⁻¹ < 1 1 < a

@[simp]
theorem ennreal.div_top {a : ennreal} :
a / = 0

@[simp]
theorem ennreal.top_div_coe {p : ℝ≥0} :

theorem ennreal.top_div_of_ne_top {a : ennreal} :
a / a =

theorem ennreal.top_div_of_lt_top {a : ennreal} :
a < / a =

theorem ennreal.top_div {a : ennreal} :
/ a = ite (a = ) 0

@[simp]
theorem ennreal.zero_div {a : ennreal} :
0 / a = 0

theorem ennreal.div_eq_top {a b : ennreal} :
a / b = a 0 b = 0 a = b

theorem ennreal.le_div_iff_mul_le {a b c : ennreal} :
b 0 c 0b c (a c / b a * b c)

theorem ennreal.div_le_iff_le_mul {a b c : ennreal} :
b 0 c b c 0(a / b c a c * b)

theorem ennreal.div_le_of_le_mul {a b c : ennreal} :
a b * ca / c b

theorem ennreal.div_lt_iff {a b c : ennreal} :
b 0 c 0b c (c / b < a c < a * b)

theorem ennreal.mul_lt_of_lt_div {a b c : ennreal} :
a < b / ca * c < b

theorem ennreal.inv_le_iff_le_mul {a b : ennreal} :
(b = a 0)(a = b 0)(a⁻¹ b 1 a * b)

@[simp]
theorem ennreal.le_inv_iff_mul_le {a b : ennreal} :
a b⁻¹ a * b 1

theorem ennreal.mul_inv_cancel {a : ennreal} :
a 0a a * a⁻¹ = 1

theorem ennreal.inv_mul_cancel {a : ennreal} :
a 0a a⁻¹ * a = 1

theorem ennreal.mul_le_iff_le_inv {a b r : ennreal} :
r 0r (r * a b a r⁻¹ * b)

theorem ennreal.le_of_forall_lt_one_mul_lt {x y : ennreal} :
(∀ (a : ennreal), a < 1a * x y)x y

theorem ennreal.div_add_div_same {a b c : ennreal} :
a / c + b / c = (a + b) / c

theorem ennreal.div_self {a : ennreal} :
a 0a a / a = 1

theorem ennreal.mul_div_cancel {a b : ennreal} :
a 0a (b / a) * a = b

theorem ennreal.mul_div_cancel' {a b : ennreal} :
a 0a a * (b / a) = b

theorem ennreal.add_halves (a : ennreal) :
a / 2 + a / 2 = a

@[simp]
theorem ennreal.div_zero_iff {a b : ennreal} :
a / b = 0 a = 0 b =

@[simp]
theorem ennreal.div_pos_iff {a b : ennreal} :
0 < a / b a 0 b

theorem ennreal.half_pos {a : ennreal} :
0 < a0 < a / 2

theorem ennreal.half_lt_self {a : ennreal} :
a 0a a / 2 < a

theorem ennreal.sub_half {a : ennreal} :
a a - a / 2 = a / 2

theorem ennreal.exists_inv_nat_lt {a : ennreal} :
a 0(∃ (n : ), (n)⁻¹ < a)

theorem ennreal.exists_nat_mul_gt {a b : ennreal} :
a 0b (∃ (n : ), b < (n) * a)

theorem ennreal.to_real_add {a b : ennreal} :
a b (a + b).to_real = a.to_real + b.to_real

theorem ennreal.of_real_add {p q : } :

@[simp]
theorem ennreal.to_real_le_to_real {a b : ennreal} :
a b (a.to_real b.to_real a b)

@[simp]
theorem ennreal.to_real_lt_to_real {a b : ennreal} :
a b (a.to_real < b.to_real a < b)

theorem ennreal.to_real_max {a b : ennreal} :
a b (max a b).to_real = max a.to_real b.to_real

theorem ennreal.to_real_pos_iff {a : ennreal} :
0 < a.to_real 0 < a a

@[simp]

@[simp]
theorem ennreal.of_real_lt_of_real_iff {p q : } :

@[simp]
theorem ennreal.of_real_pos {p : } :

@[simp]
theorem ennreal.of_real_eq_zero {p : } :

theorem ennreal.of_real_lt_iff_lt_to_real {a : } {b : ennreal} :
0 ab (ennreal.of_real a < b a < b.to_real)

theorem ennreal.le_of_real_iff_to_real_le {a : ennreal} {b : } :
a 0 b(a ennreal.of_real b a.to_real b)

theorem ennreal.to_real_le_of_le_of_real {a : ennreal} {b : } :
0 ba ennreal.of_real ba.to_real b

theorem ennreal.to_real_of_real_mul (c : ) (a : ennreal) :
0 c((ennreal.of_real c) * a).to_real = c * a.to_real

@[simp]
theorem ennreal.to_real_mul_top (a : ennreal) :
(a * ).to_real = 0

@[simp]
theorem ennreal.to_real_top_mul (a : ennreal) :
( * a).to_real = 0

theorem ennreal.to_real_eq_to_real {a b : ennreal} :
a < b < (a.to_real = b.to_real a = b)

theorem ennreal.infi_add {a : ennreal} {ι : Sort u_3} {f : ι → ennreal} :
infi f + a = ⨅ (i : ι), f i + a

theorem ennreal.supr_sub {a : ennreal} {ι : Sort u_3} {f : ι → ennreal} :
(⨆ (i : ι), f i) - a = ⨆ (i : ι), f i - a

theorem ennreal.sub_infi {a : ennreal} {ι : Sort u_3} {f : ι → ennreal} :
(a - ⨅ (i : ι), f i) = ⨆ (i : ι), a - f i

theorem ennreal.Inf_add {a : ennreal} {s : set ennreal} :
Inf s + a = ⨅ (b : ennreal) (H : b s), b + a

theorem ennreal.add_infi {ι : Sort u_3} {f : ι → ennreal} {a : ennreal} :
a + infi f = ⨅ (b : ι), a + f b

theorem ennreal.infi_add_infi {ι : Sort u_3} {f g : ι → ennreal} :
(∀ (i j : ι), ∃ (k : ι), f k + g k f i + g j)(infi f + infi g = ⨅ (a : ι), f a + g a)

theorem ennreal.infi_sum {α : Type u_1} {ι : Sort u_3} {f : ι → α → ennreal} {s : finset α} [nonempty ι] :
(∀ (t : finset α) (i j : ι), ∃ (k : ι), ∀ (a : α), a tf k a f i a f k a f j a)((⨅ (i : ι), ∑ (a : α) in s, f i a) = ∑ (a : α) in s, ⨅ (i : ι), f i a)

theorem ennreal.infi_mul {ι : Sort u_1} [nonempty ι] {f : ι → ennreal} {x : ennreal} :
x ((infi f) * x = ⨅ (i : ι), (f i) * x)

theorem ennreal.mul_infi {ι : Sort u_1} [nonempty ι] {f : ι → ennreal} {x : ennreal} :
x (x * infi f = ⨅ (i : ι), x * f i)

supr_mul, mul_supr and variants are in topology.instances.ennreal.

theorem ennreal.supr_coe_nat  :
(⨆ (n : ), n) =

theorem ennreal.le_of_add_le_add_left {a b c : ennreal} :
a < a + b a + cb c

le_of_add_le_add_left is normally applicable to ordered_cancel_add_comm_monoid, but it holds in ennreal with the additional assumption that a < ∞.