# mathlib3documentation

data.real.ennreal

# Extended non-negative reals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define `ennreal = ℝ≥0∞ := with_top ℝ≥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∞`.
@[protected, instance]
@[protected, instance]
@[protected, instance]
def ennreal  :

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

Equations
Instances for `ennreal`
@[protected, instance]
@[protected, instance]
noncomputable def ennreal.has_sub  :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable def ennreal.complete_linear_order  :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def ennreal.can_lift  :
(λ (r : ennreal), r )
Equations
@[simp]
theorem ennreal.none_eq_top  :
@[simp]
theorem ennreal.some_eq_coe (a : nnreal) :
@[protected]

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

Equations
@[protected]
def ennreal.to_real (a : ennreal) :

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

Equations
@[protected]
noncomputable def ennreal.of_real (r : ) :

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

Equations
@[simp, norm_cast]
@[simp]
@[simp]
theorem ennreal.of_real_to_real {a : ennreal} (h : a ) :
@[simp]
theorem ennreal.to_real_of_real {r : } (h : 0 r) :
= r
theorem ennreal.of_real_eq_coe_nnreal {x : } (h : 0 x) :
= x, h⟩
@[simp]
@[simp, norm_cast]
theorem ennreal.coe_zero  :
0 = 0
@[simp, norm_cast]
theorem ennreal.coe_one  :
1 = 1
@[simp]
theorem ennreal.to_real_nonneg {a : ennreal} :
@[simp]
theorem ennreal.top_to_nnreal  :
@[simp]
theorem ennreal.top_to_real  :
@[simp]
theorem ennreal.one_to_real  :
@[simp]
@[simp]
theorem ennreal.coe_to_real (r : nnreal) :
@[simp]
@[simp]
theorem ennreal.zero_to_real  :
@[simp]
theorem ennreal.of_real_zero  :
@[simp]
theorem ennreal.of_real_one  :
theorem ennreal.forall_ennreal {p : ennreal Prop} :
( (a : ennreal), p a) ( (r : nnreal), p r) p
theorem ennreal.forall_ne_top {p : ennreal Prop} :
( (a : ennreal), a p a) (r : nnreal), p r
theorem ennreal.exists_ne_top {p : ennreal Prop} :
( (a : ennreal) (H : a ), p a) (r : nnreal), p r
@[simp]
theorem ennreal.coe_ne_top {r : nnreal} :
@[simp]
theorem ennreal.top_ne_coe {r : nnreal} :
@[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.to_real_of_real_eq_iff {a : } :
= a 0 a
@[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, norm_cast]
theorem ennreal.coe_eq_coe {r q : nnreal} :
r = q r = q
@[simp, norm_cast]
theorem ennreal.coe_le_coe {r q : nnreal} :
r q r q
@[simp, norm_cast]
theorem ennreal.coe_lt_coe {r q : nnreal} :
r < q r < q
theorem ennreal.coe_mono  :
@[simp, norm_cast]
theorem ennreal.coe_eq_zero {r : nnreal} :
r = 0 r = 0
@[simp, norm_cast]
theorem ennreal.zero_eq_coe {r : nnreal} :
0 = r 0 = r
@[simp, norm_cast]
theorem ennreal.coe_eq_one {r : nnreal} :
r = 1 r = 1
@[simp, norm_cast]
theorem ennreal.one_eq_coe {r : nnreal} :
1 = r 1 = r
@[simp, norm_cast]
theorem ennreal.coe_pos {r : nnreal} :
0 < r 0 < r
theorem ennreal.coe_ne_zero {r : nnreal} :
r 0 r 0
@[simp, norm_cast]
theorem ennreal.coe_add {r p : nnreal} :
(r + p) = r + p
@[simp, norm_cast]
theorem ennreal.coe_mul {r p : nnreal} :
(r * p) = r * p
@[simp, norm_cast]
theorem ennreal.coe_bit0 {r : nnreal} :
(bit0 r) =
@[simp, norm_cast]
theorem ennreal.coe_bit1 {r : nnreal} :
(bit1 r) =
theorem ennreal.coe_two  :
2 = 2
theorem ennreal.to_nnreal_eq_to_nnreal_iff (x y : ennreal) :
x = y x = 0 y = x = y = 0
theorem ennreal.to_real_eq_to_real_iff (x y : ennreal) :
x.to_real = y.to_real x = y x = 0 y = x = y = 0
theorem ennreal.to_nnreal_eq_to_nnreal_iff' {x y : ennreal} (hx : x ) (hy : y ) :
x = y
theorem ennreal.to_real_eq_to_real_iff' {x y : ennreal} (hx : x ) (hy : y ) :
@[simp]
theorem ennreal.one_lt_two  :
1 < 2
@[protected, instance]

`(1 : ℝ≥0∞) ≤ 1`, recorded as a `fact` for use with `Lp` spaces.

@[protected, instance]

`(1 : ℝ≥0∞) ≤ 2`, recorded as a `fact` for use with `Lp` spaces.

@[protected, instance]

`(1 : ℝ≥0∞) ≤ ∞`, recorded as a `fact` for use with `Lp` spaces.

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 : ennreal α) :
( (x : {x // x }), f x) = (x : nnreal), f x
theorem ennreal.infi_ne_top {α : Type u_1} (f : ennreal α) :
( (x : ennreal) (H : x ), f x) = (x : nnreal), f x
theorem ennreal.csupr_ne_top {α : Type u_1} [has_Sup α] (f : ennreal α) :
( (x : {x // x }), f x) = (x : nnreal), f x
theorem ennreal.supr_ne_top {α : Type u_1} (f : ennreal α) :
( (x : ennreal) (H : x ), f x) = (x : nnreal), f x
theorem ennreal.infi_ennreal {α : Type u_1} {f : ennreal α} :
( (n : ennreal), f n) = ( (n : nnreal), f n) f
theorem ennreal.supr_ennreal {α : Type u_1} {f : ennreal α} :
( (n : ennreal), f n) = ( (n : nnreal), f n) f

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

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

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

Equations
theorem ennreal.smul_def {M : Type u_1} (c : nnreal) (x : M) :
c x = c x
@[protected, instance]
def ennreal.is_scalar_tower {M : Type u_1} {N : Type u_2} [ N] [ N] :
@[protected, instance]
def ennreal.smul_comm_class_left {M : Type u_1} {N : Type u_2} [ N] [ N] :
@[protected, instance]
def ennreal.smul_comm_class_right {M : Type u_1} {N : Type u_2} [ N] [ N] :
@[protected, instance]
noncomputable 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
@[protected, instance]
noncomputable def ennreal.module {M : Type u_1} [ M] :

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

Equations
@[protected, instance]
noncomputable 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} (r : R) (s : nnreal) [ nnreal] [ ennreal]  :
(r s) = r s
@[simp, norm_cast]
theorem ennreal.coe_indicator {α : Type u_1} (s : set α) (f : α nnreal) (a : α) :
(s.indicator f a) = s.indicator (λ (x : α), (f x)) a
@[simp, norm_cast]
theorem ennreal.coe_pow {r : nnreal} (n : ) :
(r ^ n) = r ^ n
@[simp]
theorem ennreal.add_eq_top {a b : ennreal} :
a + b = a = b =
@[simp]
theorem ennreal.add_lt_top {a b : ennreal} :
a + b < a < b <
theorem ennreal.to_nnreal_add {r₁ r₂ : ennreal} (h₁ : r₁ ) (h₂ : r₂ ) :
(r₁ + r₂).to_nnreal = r₁.to_nnreal + r₂.to_nnreal
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_mul_top  :
theorem ennreal.smul_top {R : Type u_1} [has_zero R] (c : R) :
c = ite (c = 0) 0
theorem ennreal.top_pow {n : } (h : 0 < n) :
theorem ennreal.mul_eq_top {a b : ennreal} :
a * b = a 0 b = a = b 0
theorem ennreal.mul_lt_top {a b : ennreal} :
a b a * b <
theorem ennreal.mul_ne_top {a b : ennreal} :
theorem ennreal.lt_top_of_mul_ne_top_left {a b : ennreal} (h : a * b ) (hb : b 0) :
a <
theorem ennreal.lt_top_of_mul_ne_top_right {a b : ennreal} (h : a * b ) (ha : a 0) :
b <
theorem ennreal.mul_lt_top_iff {a b : ennreal} :
a * b < a < b < a = 0 b = 0
theorem ennreal.mul_pos_iff {a b : ennreal} :
0 < a * b 0 < a 0 < b
theorem ennreal.mul_pos {a b : ennreal} (ha : a 0) (hb : b 0) :
0 < a * b
@[simp]
theorem ennreal.pow_eq_top_iff {a : ennreal} {n : } :
a ^ n = a = n 0
theorem ennreal.pow_eq_top {a : ennreal} (n : ) (h : a ^ n = ) :
a =
theorem ennreal.pow_ne_top {a : ennreal} (h : a ) {n : } :
a ^ n
theorem ennreal.pow_lt_top {a : ennreal} :
a < (n : ), a ^ n <
@[simp, norm_cast]
theorem ennreal.coe_finset_sum {α : Type u_1} {s : finset α} {f : α nnreal} :
(s.sum (λ (a : α), f a)) = s.sum (λ (a : α), (f a))
@[simp, norm_cast]
theorem ennreal.coe_finset_prod {α : Type u_1} {s : finset α} {f : α nnreal} :
(s.prod (λ (a : α), f a)) = s.prod (λ (a : α), (f a))
@[simp]
theorem ennreal.bot_eq_zero  :
= 0
@[simp]
theorem ennreal.coe_lt_top {r : nnreal} :
@[simp]
@[simp, norm_cast]
theorem ennreal.one_le_coe_iff {r : nnreal} :
1 r 1 r
@[simp, norm_cast]
theorem ennreal.coe_le_one_iff {r : nnreal} :
r 1 r 1
@[simp, norm_cast]
theorem ennreal.coe_lt_one_iff {p : nnreal} :
p < 1 p < 1
@[simp, norm_cast]
theorem ennreal.one_lt_coe_iff {p : nnreal} :
1 < p 1 < p
@[simp, norm_cast]
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 <
@[simp, norm_cast]
@[simp, norm_cast]
theorem ennreal.to_real_nat (n : ) :
theorem ennreal.le_coe_iff {a : ennreal} {r : nnreal} :
a r (p : nnreal), a = p p r
theorem ennreal.coe_le_iff {a : ennreal} {r : nnreal} :
r a (p : nnreal), a = p r p
theorem ennreal.lt_iff_exists_coe {a b : ennreal} :
a < b (p : nnreal), a = p p < b
@[simp, norm_cast]
theorem ennreal.coe_finset_sup {α : Type u_1} {s : finset α} {f : α nnreal} :
(s.sup f) = s.sup (λ (x : α), (f x))
@[simp]
theorem ennreal.max_eq_zero_iff {a b : ennreal} :
= 0 a = 0 b = 0
@[simp]
theorem ennreal.max_zero_left {a : ennreal} :
= a
@[simp]
theorem ennreal.max_zero_right {a : ennreal} :
= a
@[simp]
theorem ennreal.sup_eq_max {a b : ennreal} :
a b =
@[protected]
theorem ennreal.pow_pos {a : ennreal} :
0 < a (n : ), 0 < a ^ n
@[protected]
theorem ennreal.pow_ne_zero {a : ennreal} :
a 0 (n : ), a ^ n 0
@[simp]
theorem ennreal.not_lt_zero {a : ennreal} :
¬a < 0
@[protected]
a a + b a + c b c
@[protected]
a b + a c + a b c
@[protected]
a b < c a + b < a + c
@[protected]
a b < c b + a < c + a
@[protected]
a (a + b a + c b c)
@[protected]
a (b + a c + a b c)
@[protected]
a (a + b < a + c b < c)
@[protected]
a (b + a < c + a b < c)
@[protected]
a a b c < d a + c < b + d
@[protected]
c a < b c d a + c < b + d
@[protected, instance]
theorem ennreal.lt_add_right {a b : ennreal} (ha : a ) (hb : b 0) :
a < a + b
theorem ennreal.le_of_forall_pos_le_add {a b : ennreal} :
( (ε : nnreal), 0 < ε b < a b + ε) a b
theorem ennreal.lt_iff_exists_real_btwn {a b : ennreal} :
a < b (r : ), 0 r
theorem ennreal.lt_iff_exists_nnreal_btwn {a b : ennreal} :
a < b (r : nnreal), a < r r < b
theorem ennreal.lt_iff_exists_add_pos_lt {a b : ennreal} :
a < b (r : nnreal), 0 < r a + r < b
@[simp, norm_cast]
theorem ennreal.coe_nat_lt_coe {r : nnreal} {n : } :
n < r n < r
@[simp, norm_cast]
theorem ennreal.coe_lt_coe_nat {r : nnreal} {n : } :
r < n r < n
@[protected]
theorem ennreal.exists_nat_gt {r : ennreal} (h : r ) :
(n : ), r < n
@[simp]
@[simp]
@[simp]
theorem ennreal.Union_Ioc_coe_nat {a : ennreal} :
( (n : ), n) = \ {}
@[simp]
theorem ennreal.Union_Ioo_coe_nat {a : ennreal} :
( (n : ), n) = \ {}
@[simp]
theorem ennreal.Union_Icc_coe_nat {a : ennreal} :
( (n : ), n) = \ {}
@[simp]
theorem ennreal.Union_Ico_coe_nat {a : ennreal} :
( (n : ), n) = \ {}
@[simp]
theorem ennreal.Inter_Ici_coe_nat  :
( (n : ), set.Ici n) = {}
@[simp]
theorem ennreal.Inter_Ioi_coe_nat  :
( (n : ), set.Ioi n) = {}
theorem ennreal.add_lt_add {a b c d : ennreal} (ac : a < c) (bd : b < d) :
a + b < c + d
@[norm_cast]
theorem ennreal.coe_min {r p : nnreal} :
p) =
@[norm_cast]
theorem ennreal.coe_max {r p : nnreal} :
p) =
theorem ennreal.le_of_top_imp_top_of_to_nnreal_le {a b : ennreal} (h : a = b = ) (h_nnreal : a b ) :
a b
theorem ennreal.coe_Sup {s : set nnreal} :
((has_Sup.Sup s) = (a : nnreal) (H : a s), a)
theorem ennreal.coe_Inf {s : set nnreal} :
s.nonempty ((has_Inf.Inf s) = (a : nnreal) (H : a s), a)
theorem ennreal.coe_supr {ι : Sort u_1} {f : ι nnreal} (hf : bdd_above (set.range f)) :
(supr f) = (a : ι), (f a)
@[norm_cast]
theorem ennreal.coe_infi {ι : Sort u_1} [nonempty ι] (f : ι nnreal) :
(infi f) = (a : ι), (f a)
theorem ennreal.mul_lt_mul {a b c d : ennreal} (ac : a < c) (bd : b < d) :
a * b < c * d
theorem ennreal.mul_right_mono {a : ennreal} :
monotone (λ (x : ennreal), x * a)
theorem ennreal.pow_strict_mono {n : } (hn : n 0) :
strict_mono (λ (x : ennreal), x ^ n)
theorem ennreal.max_mul {a b c : ennreal} :
* c = linear_order.max (a * c) (b * c)
theorem ennreal.mul_max {a b c : ennreal} :
a * = linear_order.max (a * b) (a * c)
theorem ennreal.mul_left_strictMono {a : ennreal} (h0 : a 0) (hinf : a ) :
theorem ennreal.mul_eq_mul_left {a b c : ennreal} (h₀ : a 0) (hinf : a ) :
a * b = a * c b = c
theorem ennreal.mul_eq_mul_right {a b c : ennreal} :
c 0 c (a * c = b * c a = b)
theorem ennreal.mul_le_mul_left {a b c : ennreal} (h₀ : a 0) (hinf : a ) :
a * b a * c b c
theorem ennreal.mul_le_mul_right {a b c : ennreal} :
c 0 c (a * c b * c a b)
theorem ennreal.mul_lt_mul_left {a b c : ennreal} (h₀ : a 0) (hinf : a ) :
a * b < a * c b < c
theorem ennreal.mul_lt_mul_right {a b c : ennreal} :
c 0 c (a * c < b * c a < b)

An element `a` is `add_le_cancellable` if `a + b ≤ a + c` implies `b ≤ c` for all `b` and `c`. This is true in `ℝ≥0∞` for all elements except `∞`.

theorem ennreal.cancel_of_ne {a : ennreal} (h : a ) :

This lemma has an abbreviated name because it is used frequently.

theorem ennreal.cancel_of_lt {a : ennreal} (h : a < ) :

This lemma has an abbreviated name because it is used frequently.

theorem ennreal.cancel_of_lt' {a b : ennreal} (h : a < b) :

This lemma has an abbreviated name because it is used frequently.

theorem ennreal.cancel_coe {a : nnreal} :

This lemma has an abbreviated name because it is used frequently.

theorem ennreal.add_right_inj {a b c : ennreal} (h : a ) :
a + b = a + c b = c
theorem ennreal.add_left_inj {a b c : ennreal} (h : a ) :
b + a = c + a b = c
theorem ennreal.sub_eq_Inf {a b : ennreal} :
a - b = has_Inf.Inf {d : ennreal | a d + b}
theorem ennreal.coe_sub {r p : nnreal} :
(r - p) = r - p

This is a special case of `with_top.coe_sub` in the `ennreal` namespace

theorem ennreal.top_sub_coe {r : nnreal} :

This is a special case of `with_top.top_sub_coe` in the `ennreal` namespace

theorem ennreal.sub_top {a : ennreal} :
a - = 0

This is a special case of `with_top.sub_top` in the `ennreal` namespace

theorem ennreal.sub_eq_top_iff {a b : ennreal} :
a - b = a = b
theorem ennreal.sub_ne_top {a b : ennreal} (ha : a ) :
a - b
@[simp, norm_cast]
theorem ennreal.nat_cast_sub (m n : ) :
(m - n) = m - n
@[protected]
theorem ennreal.sub_eq_of_eq_add {a b c : ennreal} (hb : b ) :
a = c + b a - b = c
@[protected]
theorem ennreal.eq_sub_of_add_eq {a b c : ennreal} (hc : c ) :
a + c = b a = b - c
@[protected]
theorem ennreal.sub_eq_of_eq_add_rev {a b c : ennreal} (hb : b ) :
a = b + c a - b = c
theorem ennreal.sub_eq_of_add_eq {a b c : ennreal} (hb : b ) (hc : a + b = c) :
c - b = a
@[protected, simp]
theorem ennreal.add_sub_cancel_left {a b : ennreal} (ha : a ) :
a + b - a = b
@[protected, simp]
theorem ennreal.add_sub_cancel_right {a b : ennreal} (hb : b ) :
a + b - b = a
@[protected]
theorem ennreal.lt_add_of_sub_lt_left {a b c : ennreal} (h : a b ) :
a - b < c a < b + c
@[protected]
theorem ennreal.lt_add_of_sub_lt_right {a b c : ennreal} (h : a c ) :
a - c < b a < b + c
theorem ennreal.le_sub_of_add_le_left {a b c : ennreal} (ha : a ) :
a + b c b c - a
theorem ennreal.le_sub_of_add_le_right {a b c : ennreal} (hb : b ) :
a + b c a c - b
@[protected]
theorem ennreal.sub_lt_of_lt_add {a b c : ennreal} (hac : c a) (h : a < b + c) :
a - c < b
@[protected]
theorem ennreal.sub_lt_iff_lt_right {a b c : ennreal} (hb : b ) (hab : b a) :
a - b < c a < c + b
@[protected]
theorem ennreal.sub_lt_self {a b : ennreal} (ha : a ) (ha₀ : a 0) (hb : b 0) :
a - b < a
@[protected]
theorem ennreal.sub_lt_self_iff {a b : ennreal} (ha : a ) :
a - b < a 0 < a 0 < b
theorem ennreal.sub_lt_of_sub_lt {a b c : ennreal} (h₂ : c a) (h₃ : a b ) (h₁ : a - b < c) :
a - c < b
theorem ennreal.sub_sub_cancel {a b : ennreal} (h : a ) (h2 : b a) :
a - (a - b) = b
theorem ennreal.sub_right_inj {a b c : ennreal} (ha : a ) (hb : b a) (hc : c a) :
a - b = a - c b = c
theorem ennreal.sub_mul {a b c : ennreal} (h : 0 < b b < a c ) :
(a - b) * c = a * c - b * c
theorem ennreal.mul_sub {a b c : ennreal} (h : 0 < c c < b a ) :
a * (b - c) = a * b - a * c
theorem ennreal.prod_lt_top {α : Type u_1} {s : finset α} {f : α ennreal} (h : (a : α), a s f a ) :
s.prod (λ (a : α), f a) <

A product of finite numbers is still finite

theorem ennreal.sum_lt_top {α : Type u_1} {s : finset α} {f : α ennreal} (h : (a : α), a s f a ) :
s.sum (λ (a : α), f a) <

A sum of finite numbers is still finite

theorem ennreal.sum_lt_top_iff {α : Type u_1} {s : finset α} {f : α ennreal} :
s.sum (λ (a : α), f a) < (a : α), a s f a <

A sum of finite numbers is still finite

theorem ennreal.sum_eq_top_iff {α : Type u_1} {s : finset α} {f : α ennreal} :
s.sum (λ (x : α), f x) = (a : α) (H : a s), f a =

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

theorem ennreal.lt_top_of_sum_ne_top {α : Type u_1} {s : finset α} {f : α ennreal} (h : s.sum (λ (x : α), f x) ) {a : α} (ha : a s) :
f a <
theorem ennreal.to_nnreal_sum {α : Type u_1} {s : finset α} {f : α ennreal} (hf : (a : α), a s f a ) :
(s.sum (λ (a : α), f a)).to_nnreal = s.sum (λ (a : α), (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 : α ennreal} (hf : (a : α), a s f a ) :
(s.sum (λ (a : α), f a)).to_real = s.sum (λ (a : α), (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 s 0 f i) :
ennreal.of_real (s.sum (λ (i : α), f i)) = s.sum (λ (i : α), ennreal.of_real (f i))
theorem ennreal.sum_lt_sum_of_nonempty {α : Type u_1} {s : finset α} (hs : s.nonempty) {f g : α ennreal} (Hlt : (i : α), i s f i < g i) :
s.sum (λ (i : α), f i) < s.sum (λ (i : α), g i)
theorem ennreal.exists_le_of_sum_le {α : Type u_1} {s : finset α} (hs : s.nonempty) {f g : α ennreal} (Hle : s.sum (λ (i : α), f i) s.sum (λ (i : α), g i)) :
(i : α) (H : i s), f i g i
@[protected]
theorem ennreal.Ico_eq_Iio {y : ennreal} :
y =
theorem ennreal.mem_Iio_self_add {x ε : ennreal} :
x ε 0 x set.Iio (x + ε)
theorem ennreal.mem_Ioo_self_sub_add {x ε₁ ε₂ : ennreal} :
x x 0 ε₁ 0 ε₂ 0 x set.Ioo (x - ε₁) (x + ε₂)
@[simp]
theorem ennreal.bit0_lt_bit0 {a b : ennreal} :
bit0 a < bit0 b a < b
@[simp]
theorem ennreal.bit0_le_bit0 {a b : ennreal} :
bit0 a bit0 b a b
@[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_top  :
@[simp]
theorem ennreal.bit0_eq_top_iff {a : ennreal} :
@[simp]
theorem ennreal.bit1_lt_bit1 {a b : ennreal} :
bit1 a < bit1 b a < b
@[simp]
theorem ennreal.bit1_le_bit1 {a b : ennreal} :
bit1 a bit1 b a b
@[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_top  :
@[simp]
theorem ennreal.bit1_eq_top_iff {a : ennreal} :
@[simp]
theorem ennreal.bit1_eq_one_iff {a : ennreal} :
bit1 a = 1 a = 0
@[protected, instance]
noncomputable def ennreal.has_inv  :
Equations
@[protected, instance]
noncomputable def ennreal.div_inv_monoid  :
Equations
@[protected]
theorem ennreal.div_eq_inv_mul {a b : ennreal} :
a / b = b⁻¹ * a
@[simp]
theorem ennreal.inv_zero  :
@[simp]
theorem ennreal.inv_top  :
@[simp, norm_cast]
theorem ennreal.coe_inv {r : nnreal} (hr : r 0) :
@[norm_cast]
@[simp, norm_cast]
theorem ennreal.coe_div {r p : nnreal} (hr : r 0) :
(p / r) = p / r
theorem ennreal.div_zero {a : ennreal} (h : a 0) :
a / 0 =
@[protected, instance]
noncomputable def ennreal.div_inv_one_monoid  :
Equations
@[protected]
theorem ennreal.inv_pow {a : ennreal} {n : } :
(a ^ n)⁻¹ = a⁻¹ ^ n
@[protected]
theorem ennreal.mul_inv_cancel {a : ennreal} (h0 : a 0) (ht : a ) :
a * a⁻¹ = 1
@[protected]
theorem ennreal.inv_mul_cancel {a : ennreal} (h0 : a 0) (ht : a ) :
a⁻¹ * a = 1
@[protected]
theorem ennreal.div_mul_cancel {a b : ennreal} (h0 : a 0) (hI : a ) :
b / a * a = b
@[protected]
theorem ennreal.mul_div_cancel' {a b : ennreal} (h0 : a 0) (hI : a ) :
a * (b / a) = b
@[protected]
theorem ennreal.mul_comm_div {a b c : ennreal} :
a / b * c = a * (c / b)
@[protected]
theorem ennreal.mul_div_right_comm {a b c : ennreal} :
a * b / c = a / c * b
@[protected, instance]
noncomputable def ennreal.has_involutive_inv  :
Equations
@[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} (h1 : x ) (h2 : y 0) :
x / y <
@[protected, simp]
theorem ennreal.inv_eq_zero {a : ennreal} :
a⁻¹ = 0 a =
@[protected]
theorem ennreal.inv_ne_zero {a : ennreal} :
@[protected]
theorem ennreal.div_pos {a b : ennreal} (ha : a 0) (hb : b ) :
0 < a / b
@[protected]
theorem ennreal.mul_inv {a b : ennreal} (ha : a 0 b ) (hb : a b 0) :
(a * b)⁻¹ = a⁻¹ * b⁻¹
@[protected]
theorem ennreal.mul_div_mul_left {c : ennreal} (a b : ennreal) (hc : c 0) (hc' : c ) :
c * a / (c * b) = a / b
@[protected]
theorem ennreal.mul_div_mul_right {c : ennreal} (a b : ennreal) (hc : c 0) (hc' : c ) :
a * c / (b * c) = a / b
@[protected]
theorem ennreal.sub_div {a b c : ennreal} (h : 0 < b b < a c 0) :
(a - b) / c = a / c - b / c
@[protected, simp]
theorem ennreal.inv_pos {a : ennreal} :
@[protected, simp]
theorem ennreal.inv_lt_inv {a b : ennreal} :
a⁻¹ < b⁻¹ b < a
@[protected, simp]
theorem ennreal.inv_le_inv {a b : ennreal} :
@[protected, simp]
theorem ennreal.inv_le_one {a : ennreal} :
a⁻¹ 1 1 a
@[protected]
theorem ennreal.one_le_inv {a : ennreal} :
1 a⁻¹ a 1
@[protected, simp]
theorem ennreal.inv_lt_one {a : ennreal} :
a⁻¹ < 1 1 < a
@[protected, simp]
theorem ennreal.one_lt_inv {a : ennreal} :
1 < a⁻¹ a < 1
noncomputable def order_iso.inv_ennreal  :

The inverse map `λ x, x⁻¹` is an order isomorphism between `ℝ≥0∞` and its `order_dual`

Equations
@[simp]
@[simp]
theorem ennreal.div_top {a : ennreal} :
a / = 0
@[simp]
theorem ennreal.top_div_coe {p : nnreal} :
theorem ennreal.top_div_of_ne_top {a : ennreal} (h : a ) :
theorem ennreal.top_div_of_lt_top {a : ennreal} (h : a < ) :
theorem ennreal.top_div {a : ennreal} :
/ a = ite (a = ) 0
@[protected, 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
@[protected]
theorem ennreal.le_div_iff_mul_le {a b c : ennreal} (h0 : b 0 c 0) (ht : b c ) :
a c / b a * b c
@[protected]
theorem ennreal.div_le_iff_le_mul {a b c : ennreal} (hb0 : b 0 c ) (hbt : b c 0) :
a / b c a c * b
@[protected]
theorem ennreal.lt_div_iff_mul_lt {a b c : ennreal} (hb0 : b 0 c ) (hbt : b c 0) :
c < a / b c * b < a
theorem ennreal.div_le_of_le_mul {a b c : ennreal} (h : a b * c) :
a / c b
theorem ennreal.div_le_of_le_mul' {a b c : ennreal} (h : a b * c) :
a / b c
theorem ennreal.mul_le_of_le_div {a b c : ennreal} (h : a b / c) :
a * c b
theorem ennreal.mul_le_of_le_div' {a b c : ennreal} (h : a b / c) :
c * a b
@[protected]
theorem ennreal.div_lt_iff {a b c : ennreal} (h0 : b 0 c 0) (ht : b c ) :
c / b < a c < a * b
theorem ennreal.mul_lt_of_lt_div {a b c : ennreal} (h : a < b / c) :
a * c < b
theorem ennreal.mul_lt_of_lt_div' {a b c : ennreal} (h : a < b / c) :
c * a < b
theorem ennreal.inv_le_iff_le_mul {a b : ennreal} (h₁ : b = a 0) (h₂ : a = b 0) :
a⁻¹ b 1 a * b
@[simp]
theorem ennreal.le_inv_iff_mul_le {a b : ennreal} :
a b⁻¹ a * b 1
@[protected]
theorem ennreal.div_le_div {a b c d : ennreal} (hab : a b) (hdc : d c) :
a / c b / d
@[protected]
theorem ennreal.div_le_div_left {a b : ennreal} (h : a b) (c : ennreal) :
c / b c / a
@[protected]
theorem ennreal.div_le_div_right {a b : ennreal} (h : a b) (c : ennreal) :
a / c b / c
@[protected]
theorem ennreal.eq_inv_of_mul_eq_one_left {a b : ennreal} (h : a * b = 1) :
a = b⁻¹
theorem ennreal.mul_le_iff_le_inv {a b r : ennreal} (hr₀ : r 0) (hr₁ : r ) :
r * a b a r⁻¹ * b
@[protected]
theorem ennreal.le_inv_smul_iff {a b : ennreal} {r : nnreal} (hr₀ : r 0) :
a r⁻¹ b r a b

A variant of `le_inv_smul_iff` that holds for `ennreal`.

@[protected]
theorem ennreal.inv_smul_le_iff {a b : ennreal} {r : nnreal} (hr₀ : r 0) :
r⁻¹ a b a r b

A variant of `inv_smul_le_iff` that holds for `ennreal`.

theorem ennreal.le_of_forall_nnreal_lt {x y : ennreal} (h : (r : nnreal), r < x r y) :
x y
theorem ennreal.le_of_forall_pos_nnreal_lt {x y : ennreal} (h : (r : nnreal), 0 < r r < x r y) :
x y
theorem ennreal.eq_top_of_forall_nnreal_le {x : ennreal} (h : (r : nnreal), r x) :
x =
@[protected]
theorem ennreal.add_div {a b c : ennreal} :
(a + b) / c = a / c + b / c
@[protected]
theorem ennreal.div_add_div_same {a b c : ennreal} :
a / c + b / c = (a + b) / c
@[protected]
theorem ennreal.div_self {a : ennreal} (h0 : a 0) (hI : a ) :
a / a = 1
theorem ennreal.mul_div_le {a b : ennreal} :
a * (b / a) b
theorem ennreal.eq_div_iff {a b c : ennreal} (ha : a 0) (ha' : a ) :
b = c / a a * b = c
@[protected]
theorem ennreal.div_eq_div_iff {a b c d : ennreal} (ha : a 0) (ha' : a ) (hb : b 0) (hb' : b ) :
c / b = d / a a * c = b * d
theorem ennreal.div_eq_one_iff {a b : ennreal} (hb₀ : b 0) (hb₁ : b ) :
a / b = 1 a = b
@[protected, simp]
theorem ennreal.add_halves (a : ennreal) :
a / 2 + a / 2 = a
@[simp]
theorem ennreal.add_thirds (a : ennreal) :
a / 3 + a / 3 + a / 3 = 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
@[protected]
theorem ennreal.half_pos {a : ennreal} (h : a 0) :
0 < a / 2
@[protected]
@[protected]
theorem ennreal.half_lt_self {a : ennreal} (hz : a 0) (ht : a ) :
a / 2 < a
@[protected]
theorem ennreal.half_le_self {a : ennreal} :
a / 2 a
theorem ennreal.sub_half {a : ennreal} (h : a ) :
a - a / 2 = a / 2
@[simp]
noncomputable def ennreal.order_iso_Iic_one_birational  :

The birational order isomorphism between `ℝ≥0∞` and the unit interval `set.Iic (1 : ℝ≥0∞)`.

Equations
@[simp]
noncomputable def ennreal.order_iso_Iic_coe (a : nnreal) :

Order isomorphism between an initial interval in `ℝ≥0∞` and an initial interval in `ℝ≥0`.

Equations
@[simp]

An order isomorphism between the extended nonnegative real numbers and the unit interval.

Equations
@[simp]
theorem ennreal.exists_inv_nat_lt {a : ennreal} (h : a 0) :
(n : ), (n)⁻¹ < a
theorem ennreal.exists_nat_pos_mul_gt {a b : ennreal} (ha : a 0) (hb : b ) :
(n : ) (H : n > 0), b < n * a
theorem ennreal.exists_nat_mul_gt {a b : ennreal} (ha : a 0) (hb : b ) :
(n : ), b < n * a
theorem ennreal.exists_nat_pos_inv_mul_lt {a b : ennreal} (ha : a ) (hb : b 0) :
(n : ) (H : n > 0), (n)⁻¹ * a < b
theorem ennreal.exists_nnreal_pos_mul_lt {a b : ennreal} (ha : a ) (hb : b 0) :
(n : nnreal) (H : n > 0), n * a < b
theorem ennreal.exists_inv_two_pow_lt {a : ennreal} (ha : a 0) :
(n : ), 2⁻¹ ^ n < a
@[simp, norm_cast]
theorem ennreal.coe_zpow {r : nnreal} (hr : r 0) (n : ) :
(r ^ n) = r ^ n
theorem ennreal.zpow_pos {a : ennreal} (ha : a 0) (h'a : a ) (n : ) :
0 < a ^ n
theorem ennreal.zpow_lt_top {a : ennreal} (ha : a 0) (h'a : a ) (n : ) :
a ^ n <
theorem ennreal.exists_mem_Ico_zpow {x y : ennreal} (hx : x 0) (h'x : x ) (hy : 1 < y) (h'y : y ) :
(n : ), x set.Ico (y ^ n) (y ^ (n + 1))
theorem ennreal.exists_mem_Ioc_zpow {x y : ennreal} (hx : x 0) (h'x : x ) (hy : 1 < y) (h'y : y ) :
(n : ), x set.Ioc (y ^ n) (y ^ (n + 1))
theorem ennreal.Ioo_zero_top_eq_Union_Ico_zpow {y : ennreal} (hy : 1 < y) (h'y : y ) :
= (n : ), set.Ico (y ^ n) (y ^ (n + 1))
theorem ennreal.zpow_le_of_le {x : ennreal} (hx : 1 x) {a b : } (h : a b) :
x ^ a x ^ b
theorem ennreal.monotone_zpow {x : ennreal} (hx : 1 x) :
@[protected]
theorem ennreal.zpow_add {x : ennreal} (hx : x 0) (h'x : x ) (m n : ) :
x ^ (m + n) = x ^ m * x ^ n
theorem ennreal.to_real_add {a b : ennreal} (ha : a ) (hb : b ) :
theorem ennreal.to_real_sub_of_le {a b : ennreal} (h : b a) (ha : a ) :
theorem ennreal.le_to_real_sub {a b : ennreal} (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 : ennreal} (ha : a ) (hb : b ) :
theorem ennreal.to_real_mono {a b : ennreal} (hb : b ) (h : a b) :
@[simp]
theorem ennreal.to_real_lt_to_real {a b : ennreal} (ha : a ) (hb : b ) :
theorem ennreal.to_real_strict_mono {a b : ennreal} (hb : b ) (h : a < b) :
theorem ennreal.to_nnreal_mono {a b : ennreal} (hb : b ) (h : a b) :
@[simp]
theorem ennreal.to_nnreal_le_to_nnreal {a b : ennreal} (ha : a ) (hb : b ) :
a b
theorem ennreal.to_nnreal_strict_mono {a b : ennreal} (hb : b ) (h : a < b) :
@[simp]
theorem ennreal.to_nnreal_lt_to_nnreal {a b : ennreal} (ha : a ) (hb : b ) :
a < b
theorem ennreal.to_real_max {a b : ennreal} (hr : a ) (hp : b ) :
theorem ennreal.to_real_min {a b : ennreal} (hr : a ) (hp : b ) :
theorem ennreal.to_nnreal_pos {a : ennreal} (ha₀ : a 0) (ha_top : a ) :
theorem ennreal.to_real_pos_iff {a : ennreal} :
0 < a.to_real 0 < a a <
theorem ennreal.to_real_pos {a : ennreal} (ha₀ : a 0) (ha_top : a ) :
theorem ennreal.of_real_le_of_real {p q : } (h : p q) :
theorem ennreal.of_real_le_of_le_to_real {a : } {b : ennreal} (h : a b.to_real) :
@[simp]
theorem ennreal.of_real_le_of_real_iff {p q : } (h : 0 q) :
p q
@[simp]
theorem ennreal.of_real_eq_of_real_iff {p q : } (hp : 0 p) (hq : 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
@[simp]
theorem ennreal.zero_eq_of_real {p : } :
p 0
theorem ennreal.of_real_of_nonpos {p : } :
p 0

Alias of the reverse direction of `ennreal.of_real_eq_zero`.

theorem ennreal.of_real_sub (p : ) {q : } (hq : 0 q) :
theorem ennreal.of_real_le_iff_le_to_real {a : } {b : ennreal} (hb : b ) :
theorem ennreal.of_real_lt_iff_lt_to_real {a : } {b : ennreal} (ha : 0 a) (hb : b ) :
theorem ennreal.le_of_real_iff_to_real_le {a : ennreal} {b : } (ha : a ) (hb : 0 b) :
theorem ennreal.to_real_le_of_le_of_real {a : ennreal} {b : } (hb : 0 b) (h : a ) :
theorem ennreal.lt_of_real_iff_to_real_lt {a : ennreal} {b : } (ha : a ) :
theorem ennreal.of_real_mul {p q : } (hp : 0 p) :
theorem ennreal.of_real_mul' {p q : } (hq : 0 q) :
theorem ennreal.of_real_pow {p : } (hp : 0 p) (n : ) :
theorem ennreal.of_real_nsmul {x : } {n : } :
theorem ennreal.of_real_inv_of_pos {x : } (hx : 0 < x) :
theorem ennreal.of_real_div_of_pos {x y : } (hy : 0 < y) :
@[simp]
theorem ennreal.to_nnreal_mul {a b : ennreal} :
(a * b).to_nnreal =
@[simp]
theorem ennreal.smul_to_nnreal (a : nnreal) (b : ennreal) :

`ennreal.to_nnreal` as a `monoid_hom`.

Equations
@[simp]
theorem ennreal.to_nnreal_pow (a : ennreal) (n : ) :
(a ^ n).to_nnreal = a.to_nnreal ^ n
@[simp]
theorem ennreal.to_nnreal_prod {ι : Type u_1} {s : finset ι} {f : ι ennreal} :
(s.prod (λ (i : ι), f i)).to_nnreal = s.prod (λ (i : ι), (f i).to_nnreal)
noncomputable def ennreal.to_real_hom  :

`ennreal.to_real` as a `monoid_hom`.

Equations
@[simp]
theorem ennreal.to_real_mul {a b : ennreal} :
@[simp]
theorem ennreal.to_real_pow (a : ennreal) (n : ) :
(a ^ n).to_real = a.to_real ^ n
@[simp]
theorem ennreal.to_real_prod {ι : Type u_1} {s : finset ι} {f : ι ennreal} :
(s.prod (λ (i : ι), f i)).to_real = s.prod (λ (i : ι), (f i).to_real)
theorem ennreal.to_real_of_real_mul (c : ) (a : ennreal) (h : 0 c) :
* a).to_real = c * a.to_real
theorem ennreal.to_real_eq_to_real {a b : ennreal} (ha : a ) (hb : b ) :
theorem ennreal.to_real_smul (r : nnreal) (s : ennreal) :
(r s).to_real = r s.to_real
@[protected]
theorem ennreal.trichotomy (p : ennreal) :
p = 0 p = 0 < p.to_real
@[protected]
theorem ennreal.trichotomy₂ {p q : ennreal} (hpq : p q) :
p = 0 q = 0 p = 0 q = p = 0 0 < q.to_real p = q = 0 < p.to_real q = 0 < p.to_real 0 < q.to_real p.to_real q.to_real
@[protected]
theorem ennreal.dichotomy (p : ennreal) [fact (1 p)] :
theorem ennreal.to_nnreal_div (a b : ennreal) :
(a / b).to_nnreal =
theorem ennreal.to_real_div (a b : ennreal) :
theorem ennreal.of_real_prod_of_nonneg {α : Type u_1} {s : finset α} {f : α } (hf : (i : α), i s 0 f i) :
ennreal.of_real (s.prod (λ (i : α), f i)) = s.prod (λ (i : α), ennreal.of_real (f i))
@[simp]
@[simp]
theorem ennreal.to_nnreal_bit1 {x : ennreal} (hx_top : x ) :
@[simp]
theorem ennreal.to_real_bit0 {x : ennreal} :
@[simp]
theorem ennreal.to_real_bit1 {x : ennreal} (hx_top : x ) :
@[simp]
theorem ennreal.of_real_bit0 (r : ) :
=
@[simp]
theorem ennreal.of_real_bit1 {r : } (hr : 0 r) :
=
theorem ennreal.to_nnreal_infi {ι : Sort u_3} {f : ι ennreal} (hf : (i : ι), f i ) :
(infi f).to_nnreal = (i : ι), (f i).to_nnreal
theorem ennreal.to_nnreal_Inf (s : set ennreal) (hs : (r : ennreal), r s r ) :
theorem ennreal.to_nnreal_supr {ι : Sort u_3} {f : ι ennreal} (hf : (i : ι), f i ) :
(supr f).to_nnreal = (i : ι), (f i).to_nnreal
theorem ennreal.to_nnreal_Sup (s : set ennreal) (hs : (r : ennreal), r s r ) :
theorem ennreal.to_real_infi {ι : Sort u_3} {f : ι ennreal} (hf : (i : ι), f i ) :
(infi f).to_real = (i : ι), (f i).to_real
theorem ennreal.to_real_Inf (s : set ennreal) (hf : (r : ennreal), r s r ) :
theorem ennreal.to_real_supr {ι : Sort u_3} {f : ι ennreal} (hf : (i : ι), f i ) :
(supr f).to_real = (i : ι), (f i).to_real
theorem ennreal.to_real_Sup (s : set ennreal) (hf : (r : ennreal), r s r ) :
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} :
+ 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} (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 : ι } {s : finset α} [nonempty ι] (h : (t : finset α) (i j : ι), (k : ι), (a : α), a t f k a f i a f k a f j a) :
( (i : ι), s.sum (λ (a : α), f i a)) = s.sum (λ (a : α), (i : ι), f i a)
theorem ennreal.infi_mul_of_ne {ι : Sort u_1} {f : ι ennreal} {x : ennreal} (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 : ι ennreal} {x : ennreal} (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 : ι ennreal} {x : ennreal} (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 : ι ennreal} {x : ennreal} (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 : ι ennreal} :
( (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 : ennreal} :
a b = 0 a = 0 b = 0
theorem ennreal.supr_coe_nat  :
( (n : ), n) =

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

Extension for the `positivity` tactic: `ennreal.of_real` is positive if its input is.