# mathlibdocumentation

data.real.ennreal

# Extended non-negative reals #

We define ennreal = ℝ≥0∞ := 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 ℝ≥0∞ and prove basic properties of these operations, order, and conversions to/from ℝ, ℝ≥0, and ℕ.

## Main definitions #

• ℝ≥0∞: the extended nonnegative real numbers [0, ∞]; defined as with_top ℝ≥0; it is equipped with the following structures:

• coercion from ℝ≥0 defined in the natural way;

• the natural structure of a complete dense linear order: ↑p ≤ ↑q ↔ p ≤ q and ∀ a, a ≤ ∞;

• a + b is defined so that ↑p + ↑q = ↑(p + q) for (p q : ℝ≥0) and a + ∞ = ∞ + a = ∞;

• a * b is defined so that ↑p * ↑q = ↑(p * q) for (p q : ℝ≥0), 0 * ∞ = ∞ * 0 = 0, and a * ∞ = ∞ * a = ∞ for a ≠ 0;

• a - b is defined as the minimal d such that a ≤ d + b; this way we have ↑p - ↑q = ↑(p - q), ∞ - ↑p = ∞, ↑p - ∞ = ∞ - ∞ = 0; note that there is no negation, only subtraction;

• a⁻¹ is defined as Inf {b | 1 ≤ a * b}. This way we have (↑p)⁻¹ = ↑(p⁻¹) for p : ℝ≥0, p ≠ 0, 0⁻¹ = ∞, and ∞⁻¹ = 0.

• a / b is defined as a * b⁻¹.

The addition and multiplication defined this way together with 0 = ↑0 and 1 = ↑1 turn ℝ≥0∞ into a canonically ordered commutative semiring of characteristic zero.

• Coercions to/from other types:

• coercion ℝ≥0 → ℝ≥0∞ is defined as has_coe, so one can use (p : ℝ≥0) in a context that expects a : ℝ≥0∞, and Lean will apply coe automatically;

• ennreal.to_nnreal sends ↑p to p and ∞ to 0;

• ennreal.to_real := coe ∘ ennreal.to_nnreal sends ↑p, p : ℝ≥0 to (↑p : ℝ) and ∞ to 0;

• ennreal.of_real := coe ∘ real.to_nnreal sends x : ℝ to ↑⟨max x 0, _⟩

• ennreal.ne_top_equiv_nnreal is an equivalence between {a : ℝ≥0∞ // a ≠ 0} and ℝ≥0.

## Implementation notes #

We define a can_lift ℝ≥0∞ ℝ≥0 instance, so one of the ways to prove theorems about an ℝ≥0∞ 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 : α → ℝ≥0∞) (hf : ∀ x, f x ≠ ∞).

## Notations #

• ℝ≥0∞: the type of the extended nonnegative real numbers;
• ℝ≥0: the type of nonnegative real numbers [0, ∞); defined in data.real.nnreal;
• ∞: a localized notation in ℝ≥0∞ for ⊤ : ℝ≥0∞.
def ennreal  :
Type

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

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

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

Equations
• = r

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 : ℝ≥0∞} :
a (a.to_nnreal) = a
@[simp]
theorem ennreal.of_real_to_real {a : ℝ≥0∞} (h : a ) :
@[simp]
theorem ennreal.to_real_of_real {r : } (h : 0 r) :
= r
theorem ennreal.to_real_of_real' {r : } :
= max r 0
theorem ennreal.of_real_eq_coe_nnreal {x : } (h : 0 x) :
= x, h⟩
@[simp]
@[simp]
theorem ennreal.coe_zero  :
0 = 0
@[simp]
theorem ennreal.coe_one  :
1 = 1
@[simp]
@[simp]
theorem ennreal.top_to_nnreal  :
@[simp]
theorem ennreal.top_to_real  :
@[simp]
theorem ennreal.one_to_real  :
@[simp]
@[simp]
@[simp]
@[simp]
theorem ennreal.zero_to_real  :
@[simp]
theorem ennreal.of_real_zero  :
@[simp]
theorem ennreal.of_real_one  :
theorem ennreal.forall_ennreal {p : ℝ≥0∞ → Prop} :
(∀ (a : ℝ≥0∞), p a) (∀ (r : ℝ≥0), p r) p
theorem ennreal.forall_ne_top {p : ℝ≥0∞ → Prop} :
(∀ (a : ℝ≥0∞), a p a) ∀ (r : ℝ≥0), p r
theorem ennreal.exists_ne_top {p : ℝ≥0∞ → Prop} :
(∃ (a : ℝ≥0∞) (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]
theorem ennreal.of_real_ne_top {r : } :
@[simp]
theorem ennreal.of_real_lt_top {r : } :
@[simp]
theorem ennreal.top_ne_of_real {r : } :
@[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
theorem ennreal.coe_mono  :
@[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} :
(bit0 r) =
@[simp]
theorem ennreal.coe_bit1 {r : ℝ≥0} :
(bit1 r) =
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 numbers in ℝ≥0∞ that are not equal to ∞ is equivalent to ℝ≥0.

Equations
theorem ennreal.cinfi_ne_top {α : Type u_1} [has_Inf α] (f : ℝ≥0∞ → α) :
(⨅ (x : {x // x }), f x) = ⨅ (x : ℝ≥0), f x
theorem ennreal.infi_ne_top {α : Type u_1} (f : ℝ≥0∞ → α) :
(⨅ (x : ℝ≥0∞) (H : x ), f x) = ⨅ (x : ℝ≥0), f x
theorem ennreal.csupr_ne_top {α : Type u_1} [has_Sup α] (f : ℝ≥0∞ → α) :
(⨆ (x : {x // x }), f x) = ⨆ (x : ℝ≥0), f x
theorem ennreal.supr_ne_top {α : Type u_1} (f : ℝ≥0∞ → α) :
(⨆ (x : ℝ≥0∞) (H : x ), f x) = ⨆ (x : ℝ≥0), f x
theorem ennreal.infi_ennreal {α : Type u_1} {f : ℝ≥0∞ → α} :
(⨅ (n : ℝ≥0∞), f n) = (⨅ (n : ℝ≥0), f n) f
theorem ennreal.supr_ennreal {α : Type u_1} {f : ℝ≥0∞ → α} :
(⨆ (n : ℝ≥0∞), f n) = (⨆ (n : ℝ≥0), f n) f
@[simp]
theorem ennreal.add_top {a : ℝ≥0∞} :
@[simp]
theorem ennreal.top_add {a : ℝ≥0∞} :

Coercion ℝ≥0 → ℝ≥0∞ as a ring_hom.

Equations
@[simp]
@[instance]
def ennreal.mul_action {M : Type u_1} [ M] :

A mul_action over ℝ≥0∞ restricts to a mul_action over ℝ≥0.

Equations
theorem ennreal.smul_def {M : Type u_1} [ M] (c : ℝ≥0) (x : M) :
c x = c x
@[instance]
def ennreal.is_scalar_tower {M : Type u_1} {N : Type u_2} [ M] [ N] [ N] [ N] :
@[instance]
def ennreal.smul_comm_class_left {M : Type u_1} {N : Type u_2} [ N] [ N] [ N] :
@[instance]
def ennreal.smul_comm_class_right {M : Type u_1} {N : Type u_2} [ N] [ N] [ N] :
@[instance]
def ennreal.distrib_mul_action {M : Type u_1} [add_monoid M]  :

A distrib_mul_action over ℝ≥0∞ restricts to a distrib_mul_action over ℝ≥0.

Equations
@[instance]
def ennreal.module {M : Type u_1} [ M] :

A module over ℝ≥0∞ restricts to a module over ℝ≥0.

Equations
@[instance]
def ennreal.algebra {A : Type u_1} [semiring A] [ A] :

An algebra over ℝ≥0∞ restricts to an algebra over ℝ≥0.

Equations
theorem ennreal.coe_smul {R : Type u_1} [monoid R] (r : R) (s : ℝ≥0) [ ℝ≥0] [ ℝ≥0∞]  :
(r s) = r s
@[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
@[simp]
theorem ennreal.add_eq_top {a b : ℝ≥0∞} :
a + b = a = b =
@[simp]
theorem ennreal.add_lt_top {a b : ℝ≥0∞} :
a + b < a < b <
theorem ennreal.to_nnreal_add {r₁ r₂ : ℝ≥0∞} (h₁ : r₁ < ) (h₂ : r₂ < ) :
(r₁ + r₂).to_nnreal = r₁.to_nnreal + r₂.to_nnreal
theorem ennreal.bot_lt_iff_ne_bot {a : ℝ≥0∞} :
0 < a a 0
theorem ennreal.add_ne_top {a b : ℝ≥0∞} :
theorem ennreal.mul_top {a : ℝ≥0∞} :
a * = ite (a = 0) 0
theorem ennreal.top_mul {a : ℝ≥0∞} :
* a = ite (a = 0) 0
@[simp]
theorem ennreal.top_mul_top  :
theorem ennreal.top_pow {n : } (h : 0 < n) :
theorem ennreal.mul_eq_top {a b : ℝ≥0∞} :
a * b = a 0 b = a = b 0
theorem ennreal.mul_lt_top {a b : ℝ≥0∞} :
a < b < a * b <
theorem ennreal.mul_ne_top {a b : ℝ≥0∞} :
a b a * b
theorem ennreal.ne_top_of_mul_ne_top_left {a b : ℝ≥0∞} (h : a * b ) (hb : b 0) :
theorem ennreal.ne_top_of_mul_ne_top_right {a b : ℝ≥0∞} (h : a * b ) (ha : a 0) :
theorem ennreal.lt_top_of_mul_lt_top_left {a b : ℝ≥0∞} (h : a * b < ) (hb : b 0) :
a <
theorem ennreal.lt_top_of_mul_lt_top_right {a b : ℝ≥0∞} (h : a * b < ) (ha : a 0) :
b <
theorem ennreal.mul_lt_top_iff {a b : ℝ≥0∞} :
a * b < a < b < a = 0 b = 0
@[simp]
theorem ennreal.mul_pos {a b : ℝ≥0∞} :
0 < a * b 0 < a 0 < b
theorem ennreal.pow_eq_top {a : ℝ≥0∞} (n : ) :
a ^ n = a =
theorem ennreal.pow_ne_top {a : ℝ≥0∞} (h : a ) {n : } :
a ^ n
theorem ennreal.pow_lt_top {a : ℝ≥0∞} :
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.of_real_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 : ℝ≥0∞} {r : ℝ≥0} :
a r ∃ (p : ℝ≥0), a = p p r
theorem ennreal.coe_le_iff {a : ℝ≥0∞} {r : ℝ≥0} :
r a ∀ (p : ℝ≥0), a = pr p
theorem ennreal.lt_iff_exists_coe {a b : ℝ≥0∞} :
a < b ∃ (p : ℝ≥0), a = p p < b
@[simp]
theorem ennreal.coe_finset_sup {α : Type u_1} {s : finset α} {f : α → ℝ≥0} :
(s.sup f) = s.sup (λ (x : α), (f x))
theorem ennreal.pow_le_pow {a : ℝ≥0∞} {n m : } (ha : 1 a) (h : n m) :
a ^ n a ^ m
@[simp]
theorem ennreal.max_eq_zero_iff {a b : ℝ≥0∞} :
max a b = 0 a = 0 b = 0
@[simp]
theorem ennreal.max_zero_left {a : ℝ≥0∞} :
max 0 a = a
@[simp]
theorem ennreal.max_zero_right {a : ℝ≥0∞} :
max a 0 = a
@[simp]
theorem ennreal.sup_eq_max {a b : ℝ≥0∞} :
a b = max a b
theorem ennreal.pow_pos {a : ℝ≥0∞} :
0 < a∀ (n : ), 0 < a ^ n
theorem ennreal.pow_ne_zero {a : ℝ≥0∞} :
a 0∀ (n : ), a ^ n 0
@[simp]
theorem ennreal.not_lt_zero {a : ℝ≥0∞} :
¬a < 0
a < (a + c < a + b c < b)
a < (c + a < b + a c < b)
theorem ennreal.lt_add_right {a b : ℝ≥0∞} (ha : a < ) (hb : 0 < b) :
a < a + b
theorem ennreal.le_of_forall_pos_le_add {a b : ℝ≥0∞} :
(∀ (ε : ℝ≥0), 0 < εb < a b + ε)a b
theorem ennreal.lt_iff_exists_rat_btwn {a b : ℝ≥0∞} :
a < b ∃ (q : ), 0 q a < (q.to_nnreal) (q.to_nnreal) < b
theorem ennreal.lt_iff_exists_real_btwn {a b : ℝ≥0∞} :
a < b ∃ (r : ), 0 r
theorem ennreal.lt_iff_exists_nnreal_btwn {a b : ℝ≥0∞} :
a < b ∃ (r : ℝ≥0), a < r r < b
theorem ennreal.lt_iff_exists_add_pos_lt {a b : ℝ≥0∞} :
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
@[simp]
theorem ennreal.coe_nat_lt_coe_nat {m n : } :
m < n m < n
@[simp]
theorem ennreal.coe_nat_le_coe_nat {m n : } :
m n m n
@[instance]
theorem ennreal.exists_nat_gt {r : ℝ≥0∞} (h : r ) :
∃ (n : ), r < n
theorem ennreal.add_lt_add {a b c d : ℝ≥0∞} (ac : a < c) (bd : b < d) :
a + 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.le_of_top_imp_top_of_to_nnreal_le {a b : ℝ≥0∞} (h : a = b = ) (h_nnreal : a b ) :
a b
theorem ennreal.coe_Sup {s : set ℝ≥0} :
((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 : ℝ≥0∞} :
a bc da * c b * d
theorem ennreal.mul_lt_mul {a b c d : ℝ≥0∞} (ac : a < c) (bd : b < d) :
a * b < c * d
theorem ennreal.mul_right_mono {a : ℝ≥0∞} :
monotone (λ (x : ℝ≥0∞), x * a)
theorem ennreal.max_mul {a b c : ℝ≥0∞} :
(max a b) * c = max (a * c) (b * c)
theorem ennreal.mul_max {a b c : ℝ≥0∞} :
a * max b c = max (a * b) (a * c)
theorem ennreal.mul_eq_mul_left {a b c : ℝ≥0∞} :
a 0a (a * b = a * c b = c)
theorem ennreal.mul_eq_mul_right {a b c : ℝ≥0∞} :
c 0c (a * c = b * c a = b)
theorem ennreal.mul_le_mul_left {a b c : ℝ≥0∞} :
a 0a (a * b a * c b c)
theorem ennreal.mul_le_mul_right {a b c : ℝ≥0∞} :
c 0c (a * c b * c a b)
theorem ennreal.mul_lt_mul_left {a b c : ℝ≥0∞} :
a 0a (a * b < a * c b < c)
theorem ennreal.mul_lt_mul_right {a b c : ℝ≥0∞} :
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 : ℝ≥0∞} (h : a b) :
a - b = 0
@[simp]
theorem ennreal.sub_self {a : ℝ≥0∞} :
a - a = 0
@[simp]
theorem ennreal.zero_sub {a : ℝ≥0∞} :
0 - a = 0
@[simp]
theorem ennreal.sub_infty {a : ℝ≥0∞} :
a - = 0
theorem ennreal.sub_le_sub {a b c d : ℝ≥0∞} (h₁ : a b) (h₂ : d c) :
a - c b - d
@[simp]
theorem ennreal.add_sub_self {a b : ℝ≥0∞} :
b < a + b - b = a
@[simp]
theorem ennreal.add_sub_self' {a b : ℝ≥0∞} (h : a < ) :
a + b - a = b
theorem ennreal.add_right_inj {a b c : ℝ≥0∞} (h : a < ) :
a + b = a + c b = c
theorem ennreal.add_left_inj {a b c : ℝ≥0∞} (h : a < ) :
b + a = c + a b = c
@[simp]
theorem ennreal.sub_add_cancel_of_le {a b : ℝ≥0∞} :
b aa - b + b = a
@[simp]
theorem ennreal.add_sub_cancel_of_le {a b : ℝ≥0∞} (h : b a) :
b + (a - b) = a
theorem ennreal.sub_add_self_eq_max {a b : ℝ≥0∞} :
a - b + b = max a b
theorem ennreal.le_sub_add_self {a b : ℝ≥0∞} :
a a - b + b
@[simp]
theorem ennreal.sub_le_iff_le_add {a b c : ℝ≥0∞} :
a - b c a c + b
theorem ennreal.sub_le_iff_le_add' {a b c : ℝ≥0∞} :
a - b c a b + c
theorem ennreal.sub_eq_of_add_eq {a b c : ℝ≥0∞} :
b a + b = cc - b = a
theorem ennreal.sub_le_of_sub_le {a b c : ℝ≥0∞} (h : a - b c) :
a - c b
theorem ennreal.sub_lt_self {a b : ℝ≥0∞} :
a a 00 < ba - b < a
@[simp]
theorem ennreal.sub_eq_zero_iff_le {a b : ℝ≥0∞} :
a - b = 0 a b
@[simp]
theorem ennreal.zero_lt_sub_iff_lt {a b : ℝ≥0∞} :
0 < a - b b < a
theorem ennreal.lt_sub_iff_add_lt {a b c : ℝ≥0∞} :
a < b - c a + c < b
theorem ennreal.sub_le_self (a b : ℝ≥0∞) :
a - b a
@[simp]
theorem ennreal.sub_zero {a : ℝ≥0∞} :
a - 0 = a
theorem ennreal.sub_le_sub_add_sub {a b c : ℝ≥0∞} :
a - c a - b + (b - c)

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

theorem ennreal.sub_sub_cancel {a b : ℝ≥0∞} (h : a < ) (h2 : b a) :
a - (a - b) = b
theorem ennreal.sub_right_inj {a b c : ℝ≥0∞} (ha : a < ) (hb : b a) (hc : c a) :
a - b = a - c b = c
theorem ennreal.sub_mul {a b c : ℝ≥0∞} (h : 0 < bb < ac ) :
(a - b) * c = a * c - b * c
theorem ennreal.mul_sub {a b c : ℝ≥0∞} (h : 0 < cc < ba ) :
a * (b - c) = a * b - a * c
theorem ennreal.sub_mul_ge {a b c : ℝ≥0∞} :
a * c - b * c (a - b) * c
theorem ennreal.prod_lt_top {α : Type u_1} {s : finset α} {f : α → ℝ≥0∞} (h : ∀ (a : α), a sf a < ) :
∏ (a : α) in s, f a <

A product of finite numbers is still finite

theorem ennreal.sum_lt_top {α : Type u_1} {s : finset α} {f : α → ℝ≥0∞} :
(∀ (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 : α → ℝ≥0∞} :
∑ (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 : α → ℝ≥0∞} :
∑ (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 : α → ℝ≥0∞} (hf : ∀ (a : α), a sf a < ) :
(∑ (a : α) in s, f a).to_nnreal = ∑ (a : α) in s, (f a).to_nnreal

seeing ℝ≥0∞ as ℝ≥0 does not change their sum, unless one of the ℝ≥0∞ is infinity

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

seeing ℝ≥0∞ as real does not change their sum, unless one of the ℝ≥0∞ is infinity

theorem ennreal.of_real_sum_of_nonneg {α : Type u_1} {s : finset α} {f : α → } (hf : ∀ (i : α), i s0 f i) :
ennreal.of_real (∑ (i : α) in s, f i) = ∑ (i : α) in s, ennreal.of_real (f i)
theorem ennreal.Ico_eq_Iio {y : ℝ≥0∞} :
y =
theorem ennreal.mem_Iio_self_add {x ε : ℝ≥0∞} :
x 0 < εx set.Iio (x + ε)
theorem ennreal.not_mem_Ioo_self_sub {x y ε : ℝ≥0∞} :
x = 0x set.Ioo (x - ε) y
theorem ennreal.mem_Ioo_self_sub_add {x ε₁ ε₂ : ℝ≥0∞} :
x x 00 < ε₁0 < ε₂x set.Ioo (x - ε₁) (x + ε₂)
@[simp]
theorem ennreal.bit0_inj {a b : ℝ≥0∞} :
bit0 a = bit0 b a = b
@[simp]
theorem ennreal.bit0_eq_zero_iff {a : ℝ≥0∞} :
bit0 a = 0 a = 0
@[simp]
@[simp]
theorem ennreal.bit1_inj {a b : ℝ≥0∞} :
bit1 a = bit1 b a = b
@[simp]
theorem ennreal.bit1_ne_zero {a : ℝ≥0∞} :
bit1 a 0
@[simp]
theorem ennreal.bit1_eq_one_iff {a : ℝ≥0∞} :
bit1 a = 1 a = 0
@[simp]
@[instance]
Equations
@[instance]
Equations
@[simp]
theorem ennreal.inv_zero  :
@[simp]
theorem ennreal.inv_top  :
@[simp]
theorem ennreal.coe_inv {r : ℝ≥0} (hr : r 0) :
@[simp]
theorem ennreal.coe_div {r p : ℝ≥0} (hr : r 0) :
(p / r) = p / r
@[simp]
theorem ennreal.inv_one  :
1⁻¹ = 1
@[simp]
theorem ennreal.div_one {a : ℝ≥0∞} :
a / 1 = a
theorem ennreal.inv_pow {a : ℝ≥0∞} {n : } :
(a ^ n)⁻¹ = a⁻¹ ^ n
@[simp]
theorem ennreal.inv_inv {a : ℝ≥0∞} :
@[simp]
theorem ennreal.inv_eq_inv {a b : ℝ≥0∞} :
a⁻¹ = b⁻¹ a = b
@[simp]
theorem ennreal.inv_eq_top {a : ℝ≥0∞} :
a⁻¹ = a = 0
@[simp]
theorem ennreal.inv_lt_top {x : ℝ≥0∞} :
x⁻¹ < 0 < x
theorem ennreal.div_lt_top {x y : ℝ≥0∞} (h1 : x < ) (h2 : 0 < y) :
x / y <
@[simp]
theorem ennreal.inv_eq_zero {a : ℝ≥0∞} :
a⁻¹ = 0 a =
@[simp]
theorem ennreal.inv_pos {a : ℝ≥0∞} :
@[simp]
theorem ennreal.inv_lt_inv {a b : ℝ≥0∞} :
a⁻¹ < b⁻¹ b < a
@[simp]
theorem ennreal.inv_le_inv {a b : ℝ≥0∞} :
@[simp]
theorem ennreal.inv_le_one {a : ℝ≥0∞} :
a⁻¹ 1 1 a
theorem ennreal.one_le_inv {a : ℝ≥0∞} :
1 a⁻¹ a 1
@[simp]
theorem ennreal.inv_lt_one {a : ℝ≥0∞} :
a⁻¹ < 1 1 < a
theorem ennreal.pow_le_pow_of_le_one {a : ℝ≥0∞} {n m : } (ha : a 1) (h : n m) :
a ^ m a ^ n
@[simp]
theorem ennreal.div_top {a : ℝ≥0∞} :
a / = 0
@[simp]
theorem ennreal.top_div_coe {p : ℝ≥0} :
theorem ennreal.top_div_of_ne_top {a : ℝ≥0∞} (h : a ) :
theorem ennreal.top_div_of_lt_top {a : ℝ≥0∞} (h : a < ) :
theorem ennreal.top_div {a : ℝ≥0∞} :
/ a = ite (a = ) 0
@[simp]
theorem ennreal.zero_div {a : ℝ≥0∞} :
0 / a = 0
theorem ennreal.div_eq_top {a b : ℝ≥0∞} :
a / b = a 0 b = 0 a = b
theorem ennreal.le_div_iff_mul_le {a b c : ℝ≥0∞} (h0 : b 0 c 0) (ht : b c ) :
a c / b a * b c
theorem ennreal.div_le_iff_le_mul {a b c : ℝ≥0∞} (hb0 : b 0 c ) (hbt : b c 0) :
a / b c a c * b
theorem ennreal.div_le_of_le_mul {a b c : ℝ≥0∞} (h : a b * c) :
a / c b
theorem ennreal.div_lt_iff {a b c : ℝ≥0∞} (h0 : b 0 c 0) (ht : b c ) :
c / b < a c < a * b
theorem ennreal.mul_lt_of_lt_div {a b c : ℝ≥0∞} (h : a < b / c) :
a * c < b
theorem ennreal.inv_le_iff_le_mul {a b : ℝ≥0∞} :
(b = a 0)(a = b 0)(a⁻¹ b 1 a * b)
@[simp]
theorem ennreal.le_inv_iff_mul_le {a b : ℝ≥0∞} :
a b⁻¹ a * b 1
theorem ennreal.mul_inv_cancel {a : ℝ≥0∞} (h0 : a 0) (ht : a ) :
a * a⁻¹ = 1
theorem ennreal.inv_mul_cancel {a : ℝ≥0∞} (h0 : a 0) (ht : a ) :
a⁻¹ * a = 1
theorem ennreal.eq_inv_of_mul_eq_one {a b : ℝ≥0∞} (h : a * b = 1) :
a = b⁻¹
theorem ennreal.mul_le_iff_le_inv {a b r : ℝ≥0∞} (hr₀ : r 0) (hr₁ : r ) :
r * a b a r⁻¹ * b
theorem ennreal.le_of_forall_nnreal_lt {x y : ℝ≥0∞} (h : ∀ (r : ℝ≥0), r < xr y) :
x y
theorem ennreal.le_of_forall_pos_nnreal_lt {x y : ℝ≥0∞} (h : ∀ (r : ℝ≥0), 0 < rr < xr y) :
x y
theorem ennreal.eq_top_of_forall_nnreal_le {x : ℝ≥0∞} (h : ∀ (r : ℝ≥0), r x) :
x =
theorem ennreal.div_add_div_same {a b c : ℝ≥0∞} :
a / c + b / c = (a + b) / c
theorem ennreal.div_self {a : ℝ≥0∞} (h0 : a 0) (hI : a ) :
a / a = 1
theorem ennreal.mul_div_cancel {a b : ℝ≥0∞} (h0 : a 0) (hI : a ) :
(b / a) * a = b
theorem ennreal.mul_div_cancel' {a b : ℝ≥0∞} (h0 : a 0) (hI : a ) :
a * (b / a) = b
theorem ennreal.mul_div_le {a b : ℝ≥0∞} :
a * (b / a) b
theorem ennreal.add_halves (a : ℝ≥0∞) :
a / 2 + a / 2 = a
@[simp]
theorem ennreal.div_zero_iff {a b : ℝ≥0∞} :
a / b = 0 a = 0 b =
@[simp]
theorem ennreal.div_pos_iff {a b : ℝ≥0∞} :
0 < a / b a 0 b
theorem ennreal.half_pos {a : ℝ≥0∞} (h : 0 < a) :
0 < a / 2
theorem ennreal.half_lt_self {a : ℝ≥0∞} (hz : a 0) (ht : a ) :
a / 2 < a
theorem ennreal.sub_half {a : ℝ≥0∞} (h : a ) :
a - a / 2 = a / 2
@[simp]
theorem ennreal.exists_inv_nat_lt {a : ℝ≥0∞} (h : a 0) :
∃ (n : ), (n)⁻¹ < a
theorem ennreal.exists_nat_pos_mul_gt {a b : ℝ≥0∞} (ha : a 0) (hb : b ) :
∃ (n : ) (H : n > 0), b < (n) * a
theorem ennreal.exists_nat_mul_gt {a b : ℝ≥0∞} (ha : a 0) (hb : b ) :
∃ (n : ), b < (n) * a
theorem ennreal.exists_nat_pos_inv_mul_lt {a b : ℝ≥0∞} (ha : a ) (hb : b 0) :
∃ (n : ) (H : n > 0), (n)⁻¹ * a < b
theorem ennreal.exists_nnreal_pos_mul_lt {a b : ℝ≥0∞} (ha : a ) (hb : b 0) :
∃ (n : ℝ≥0) (H : n > 0), (n) * a < b
theorem ennreal.exists_inv_two_pow_lt {a : ℝ≥0∞} (ha : a 0) :
∃ (n : ), 2⁻¹ ^ n < a
theorem ennreal.to_real_add {a b : ℝ≥0∞} (ha : a ) (hb : b ) :
theorem ennreal.of_real_add {p q : } (hp : 0 p) (hq : 0 q) :
@[simp]
theorem ennreal.to_real_le_to_real {a b : ℝ≥0∞} (ha : a ) (hb : b ) :
theorem ennreal.to_real_mono {a b : ℝ≥0∞} (hb : b ) (h : a b) :
@[simp]
theorem ennreal.to_real_lt_to_real {a b : ℝ≥0∞} (ha : a ) (hb : b ) :
theorem ennreal.to_real_strict_mono {a b : ℝ≥0∞} (hb : b ) (h : a < b) :
theorem ennreal.to_real_max {a b : ℝ≥0∞} (hr : a ) (hp : b ) :
theorem ennreal.of_real_le_of_real {p q : } (h : p q) :
@[simp]
theorem ennreal.of_real_le_of_real_iff {p q : } (h : 0 q) :
p q
@[simp]
theorem ennreal.of_real_lt_of_real_iff {p q : } (h : 0 < q) :
p < q
theorem ennreal.of_real_lt_of_real_iff_of_nonneg {p q : } (hp : 0 p) :
p < q
@[simp]
theorem ennreal.of_real_pos {p : } :
0 < p
@[simp]
theorem ennreal.of_real_eq_zero {p : } :
p 0
theorem ennreal.of_real_lt_iff_lt_to_real {a : } {b : ℝ≥0∞} (ha : 0 a) (hb : b ) :
theorem ennreal.le_of_real_iff_to_real_le {a : ℝ≥0∞} {b : } (ha : a ) (hb : 0 b) :
theorem ennreal.to_real_le_of_le_of_real {a : ℝ≥0∞} {b : } (hb : 0 b) (h : a ) :
theorem ennreal.lt_of_real_iff_to_real_lt {a : ℝ≥0∞} {b : } (ha : a ) :
theorem ennreal.of_real_mul {p q : } (hp : 0 p) :
theorem ennreal.of_real_inv_of_pos {x : } (hx : 0 < x) :
theorem ennreal.of_real_div_of_pos {x y : } (hy : 0 < y) :
theorem ennreal.to_real_of_real_mul (c : ) (a : ℝ≥0∞) (h : 0 c) :
@[simp]
@[simp]
@[simp]
theorem ennreal.to_real_mul_top (a : ℝ≥0∞) :
(a * ).to_real = 0
@[simp]
theorem ennreal.to_real_top_mul (a : ℝ≥0∞) :
( * a).to_real = 0
theorem ennreal.to_real_eq_to_real {a b : ℝ≥0∞} (ha : a < ) (hb : b < ) :
theorem ennreal.to_real_smul (r : ℝ≥0) (s : ℝ≥0∞) :
(r s).to_real = r s.to_real

ennreal.to_nnreal as a monoid_hom.

Equations
theorem ennreal.to_nnreal_pow (a : ℝ≥0∞) (n : ) :
(a ^ n).to_nnreal = a.to_nnreal ^ n
theorem ennreal.to_nnreal_prod {ι : Type u_1} {s : finset ι} {f : ι → ℝ≥0∞} :
(∏ (i : ι) in s, f i).to_nnreal = ∏ (i : ι) in s, (f i).to_nnreal

ennreal.to_real as a monoid_hom.

Equations
theorem ennreal.to_real_mul {a b : ℝ≥0∞} :
(a * b).to_real = (a.to_real) * b.to_real
theorem ennreal.to_real_pow (a : ℝ≥0∞) (n : ) :
(a ^ n).to_real = a.to_real ^ n
theorem ennreal.to_real_prod {ι : Type u_1} {s : finset ι} {f : ι → ℝ≥0∞} :
(∏ (i : ι) in s, f i).to_real = ∏ (i : ι) in s, (f i).to_real
theorem ennreal.of_real_prod_of_nonneg {α : Type u_1} {s : finset α} {f : α → } (hf : ∀ (i : α), i s0 f i) :
ennreal.of_real (∏ (i : α) in s, f i) = ∏ (i : α) in s, ennreal.of_real (f i)
@[simp]
@[simp]
theorem ennreal.to_nnreal_bit1 {x : ℝ≥0∞} (hx_top : x ) :
@[simp]
@[simp]
theorem ennreal.to_real_bit1 {x : ℝ≥0∞} (hx_top : x ) :
@[simp]
theorem ennreal.of_real_bit0 {r : } (hr : 0 r) :
=
@[simp]
theorem ennreal.of_real_bit1 {r : } (hr : 0 r) :
=
theorem ennreal.infi_add {a : ℝ≥0∞} {ι : Sort u_3} {f : ι → ℝ≥0∞} :
infi f + a = ⨅ (i : ι), f i + a
theorem ennreal.supr_sub {a : ℝ≥0∞} {ι : Sort u_3} {f : ι → ℝ≥0∞} :
(⨆ (i : ι), f i) - a = ⨆ (i : ι), f i - a
theorem ennreal.sub_infi {a : ℝ≥0∞} {ι : Sort u_3} {f : ι → ℝ≥0∞} :
(a - ⨅ (i : ι), f i) = ⨆ (i : ι), a - f i
theorem ennreal.Inf_add {a : ℝ≥0∞} {s : set ℝ≥0∞} :
Inf s + a = ⨅ (b : ℝ≥0∞) (H : b s), b + a
theorem ennreal.add_infi {ι : Sort u_3} {f : ι → ℝ≥0∞} {a : ℝ≥0∞} :
a + infi f = ⨅ (b : ι), a + f b
theorem ennreal.infi_add_infi {ι : Sort u_3} {f g : ι → ℝ≥0∞} (h : ∀ (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 : ι → α → ℝ≥0∞} {s : finset α} [nonempty ι] (h : ∀ (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_of_ne {ι : Sort u_1} {f : ι → ℝ≥0∞} {x : ℝ≥0∞} (h0 : x 0) (h : x ) :
(infi f) * x = ⨅ (i : ι), (f i) * x

If x ≠ 0 and x ≠ ∞, then right multiplication by x maps infimum to infimum. See also ennreal.infi_mul that assumes [nonempty ι] but does not require x ≠ 0.

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

If x ≠ ∞, then right multiplication by x maps infimum over a nonempty type to infimum. See also ennreal.infi_mul_of_ne that assumes x ≠ 0 but does not require [nonempty ι].

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

If x ≠ ∞, then left multiplication by x maps infimum over a nonempty type to infimum. See also ennreal.mul_infi_of_ne that assumes x ≠ 0 but does not require [nonempty ι].

theorem ennreal.mul_infi_of_ne {ι : Sort u_1} {f : ι → ℝ≥0∞} {x : ℝ≥0∞} (h0 : x 0) (h : x ) :
x * infi f = ⨅ (i : ι), x * f i

If x ≠ 0 and x ≠ ∞, then left multiplication by x maps infimum to infimum. See also ennreal.mul_infi that assumes [nonempty ι] but does not require x ≠ 0.

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

@[simp]
theorem ennreal.supr_eq_zero {ι : Sort u_1} {f : ι → ℝ≥0∞} :
(⨆ (i : ι), f i) = 0 ∀ (i : ι), f i = 0
@[simp]
theorem ennreal.supr_zero_eq_zero {ι : Sort u_1} :
(⨆ (i : ι), 0) = 0
theorem ennreal.sup_eq_zero {a b : ℝ≥0∞} :
a b = 0 a = 0 b = 0
theorem ennreal.supr_coe_nat  :
(⨆ (n : ), n) =
le_of_add_le_add_left is normally applicable to ordered_cancel_add_comm_monoid, but it holds in ℝ≥0∞ with the additional assumption that a < ∞.
le_of_add_le_add_right is normally applicable to ordered_cancel_add_comm_monoid, but it holds in ℝ≥0∞ with the additional assumption that a < ∞.