mathlib documentation

data.real.ennreal

Extended non-negative reals #

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]

noncomputable def ennreal.linear_ordered_add_comm_monoid_with_top :

linear_ordered_add_comm_monoid_with_top ℝ≥0∞

@[protected, instance]

noncomputable def ennreal.has_ordered_sub :

has_ordered_sub ℝ≥0∞

def ennreal :

Type

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

Equations

ℝ≥0∞ = with_top ℝ≥0

@[protected, instance]

noncomputable def ennreal.has_sub :

has_sub ℝ≥0∞

@[protected, instance]

def ennreal.add_comm_monoid :

add_comm_monoid ℝ≥0∞

@[protected, instance]

def ennreal.nontrivial :

nontrivial ℝ≥0∞

@[protected, instance]

def ennreal.has_zero :

has_zero ℝ≥0∞

@[protected, instance]

def ennreal.densely_ordered :

densely_ordered ℝ≥0∞

@[protected, instance]

noncomputable def ennreal.canonically_ordered_comm_semiring :

canonically_ordered_comm_semiring ℝ≥0∞

@[protected, instance]

noncomputable def ennreal.complete_linear_order :

complete_linear_order ℝ≥0∞

@[protected, instance]

noncomputable def ennreal.canonically_linear_ordered_add_monoid :

canonically_linear_ordered_add_monoid ℝ≥0∞

@[protected, instance]

def ennreal.covariant_class_mul_le :

covariant_class ℝ≥0∞ ℝ≥0∞ has_mul.mul has_le.le

@[protected, instance]

def ennreal.covariant_class_add_le :

covariant_class ℝ≥0∞ ℝ≥0∞ has_add.add has_le.le

@[protected, instance]

def ennreal.inhabited :

inhabited ℝ≥0∞

Equations

ennreal.inhabited = {default := 0}

@[protected, instance]

def ennreal.has_coe :

has_coe ℝ≥0 ℝ≥0∞

Equations

ennreal.has_coe = {coe := some ℝ≥0}

@[protected, instance]

def ennreal.nnreal.can_lift :

can_lift ℝ≥0∞ ℝ≥0

Equations

ennreal.nnreal.can_lift = {coe := coe coe_to_lift, cond := λ (r : ℝ≥0∞), r ≠ ⊤, prf := ennreal.nnreal.can_lift._proof_1}

@[simp]

theorem ennreal.none_eq_top :

@[simp]

theorem ennreal.some_eq_coe (a : ℝ≥0) :

@[protected]

def ennreal.to_nnreal :

ℝ≥0∞ → ℝ≥0

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

Equations

ennreal.to_nnreal (some r) = r
ennreal.to_nnreal none = 0

@[protected]

def ennreal.to_real (a : ℝ≥0∞) :

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

Equations

a.to_real = ↑(a.to_nnreal)

@[protected]

noncomputable def ennreal.of_real (r : ℝ) :

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

Equations

ennreal.of_real r = ↑(r.to_nnreal)

@[simp, norm_cast]

theorem ennreal.to_nnreal_coe {r : ℝ≥0} :

↑r.to_nnreal = r

@[simp]

theorem ennreal.coe_to_nnreal {a : ℝ≥0∞} :

a ≠ ⊤ → ↑(a.to_nnreal) = a

@[simp]

theorem ennreal.of_real_to_real {a : ℝ≥0∞} (h : a ≠ ⊤) :

ennreal.of_real a.to_real = a

@[simp]

theorem ennreal.to_real_of_real {r : ℝ} (h : 0 ≤ r) :

(ennreal.of_real r).to_real = r

theorem ennreal.to_real_of_real' {r : ℝ} :

(ennreal.of_real r).to_real = max r 0

theorem ennreal.coe_to_nnreal_le_self {a : ℝ≥0∞} :

↑(a.to_nnreal) ≤ a

theorem ennreal.coe_nnreal_eq (r : ℝ≥0) :

↑r = ennreal.of_real ↑r

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

ennreal.of_real x = ↑⟨x, h⟩

@[simp]

theorem ennreal.of_real_coe_nnreal {p : ℝ≥0} :

ennreal.of_real ↑p = ↑p

@[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 : ℝ≥0∞} :

0 ≤ a.to_real

@[simp]

theorem ennreal.top_to_nnreal :

⊤.to_nnreal = 0

@[simp]

theorem ennreal.top_to_real :

⊤.to_real = 0

@[simp]

theorem ennreal.one_to_real :

@[simp]

theorem ennreal.one_to_nnreal :

1.to_nnreal = 1

@[simp]

theorem ennreal.coe_to_real (r : ℝ≥0) :

↑r.to_real = ↑r

@[simp]

theorem ennreal.zero_to_nnreal :

0.to_nnreal = 0

@[simp]

theorem ennreal.zero_to_real :

@[simp]

theorem ennreal.of_real_zero :

ennreal.of_real 0 = 0

@[simp]

theorem ennreal.of_real_one :

ennreal.of_real 1 = 1

theorem ennreal.of_real_to_real_le {a : ℝ≥0∞} :

ennreal.of_real a.to_real ≤ a

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

theorem ennreal.to_nnreal_eq_zero_iff (x : ℝ≥0∞) :

x.to_nnreal = 0 ↔ x = 0 ∨ x = ⊤

theorem ennreal.to_real_eq_zero_iff (x : ℝ≥0∞) :

x.to_real = 0 ↔ x = 0 ∨ x = ⊤

@[simp]

theorem ennreal.coe_ne_top {r : ℝ≥0} :

@[simp]

theorem ennreal.top_ne_coe {r : ℝ≥0} :

@[simp]

theorem ennreal.of_real_ne_top {r : ℝ} :

ennreal.of_real r ≠ ⊤

@[simp]

theorem ennreal.of_real_lt_top {r : ℝ} :

ennreal.of_real r < ⊤

@[simp]

theorem ennreal.top_ne_of_real {r : ℝ} :

⊤ ≠ ennreal.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, norm_cast]

theorem ennreal.coe_eq_coe {r q : ℝ≥0} :

↑r = ↑q ↔ r = q

@[simp, norm_cast]

theorem ennreal.coe_le_coe {r q : ℝ≥0} :

↑r ≤ ↑q ↔ r ≤ q

@[simp, norm_cast]

theorem ennreal.coe_lt_coe {r q : ℝ≥0} :

↑r < ↑q ↔ r < q

theorem ennreal.coe_mono :

@[simp, norm_cast]

theorem ennreal.coe_eq_zero {r : ℝ≥0} :

↑r = 0 ↔ r = 0

@[simp, norm_cast]

theorem ennreal.zero_eq_coe {r : ℝ≥0} :

0 = ↑r ↔ 0 = r

@[simp, norm_cast]

theorem ennreal.coe_eq_one {r : ℝ≥0} :

↑r = 1 ↔ r = 1

@[simp, norm_cast]

theorem ennreal.one_eq_coe {r : ℝ≥0} :

1 = ↑r ↔ 1 = r

@[simp, norm_cast]

theorem ennreal.coe_nonneg {r : ℝ≥0} :

0 ≤ ↑r ↔ 0 ≤ r

@[simp, norm_cast]

theorem ennreal.coe_pos {r : ℝ≥0} :

0 < ↑r ↔ 0 < r

theorem ennreal.coe_ne_zero {r : ℝ≥0} :

↑r ≠ 0 ↔ r ≠ 0

@[simp, norm_cast]

theorem ennreal.coe_add {r p : ℝ≥0} :

↑(r + p) = ↑r + ↑p

@[simp, norm_cast]

theorem ennreal.coe_mul {r p : ℝ≥0} :

↑r * p = (↑r) * ↑p

@[simp, norm_cast]

theorem ennreal.coe_bit0 {r : ℝ≥0} :

↑(bit0 r) = bit0 ↑r

@[simp, norm_cast]

theorem ennreal.coe_bit1 {r : ℝ≥0} :

↑(bit1 r) = bit1 ↑r

theorem ennreal.coe_two :

↑2 = 2

@[protected]

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

theorem ennreal.two_ne_top :

@[protected, instance]

def fact_one_le_one_ennreal :

fact (1 ≤ 1)

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

@[protected, instance]

def fact_one_le_two_ennreal :

fact (1 ≤ 2)

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

@[protected, instance]

def fact_one_le_top_ennreal :

fact (1 ≤ ⊤)

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

def ennreal.ne_top_equiv_nnreal :

↥{a : ℝ≥0∞ | a ≠ ⊤} ≃ ℝ≥0

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

Equations

ennreal.ne_top_equiv_nnreal = {to_fun := λ (x : ↥{a : ℝ≥0∞ | a ≠ ⊤}), ↑x.to_nnreal, inv_fun := λ (x : ℝ≥0), ⟨↑x, _⟩, left_inv := ennreal.ne_top_equiv_nnreal._proof_1, right_inv := ennreal.ne_top_equiv_nnreal._proof_2}

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} [complete_lattice α] (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} [complete_lattice α] (f : ℝ≥0∞ → α) :

(⨆ (x : ℝ≥0∞) (H : x ≠ ⊤), f x) = ⨆ (x : ℝ≥0), f ↑x

theorem ennreal.infi_ennreal {α : Type u_1} [complete_lattice α] {f : ℝ≥0∞ → α} :

(⨅ (n : ℝ≥0∞), f n) = (⨅ (n : ℝ≥0), f ↑n) ⊓ f ⊤

theorem ennreal.supr_ennreal {α : Type u_1} [complete_lattice α] {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∞} :

def ennreal.of_nnreal_hom :

ℝ≥0 →+* ℝ≥0∞

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

Equations

ennreal.of_nnreal_hom = {to_fun := coe coe_to_lift, map_one' := ennreal.coe_one, map_mul' := ennreal.of_nnreal_hom._proof_1, map_zero' := ennreal.coe_zero, map_add' := ennreal.of_nnreal_hom._proof_2}

@[simp]

theorem ennreal.coe_of_nnreal_hom :

⇑ennreal.of_nnreal_hom = coe

@[protected, instance]

noncomputable def ennreal.mul_action {M : Type u_1} [mul_action ℝ≥0∞ M] :

mul_action ℝ≥0 M

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

Equations

ennreal.mul_action = mul_action.comp_hom M ennreal.of_nnreal_hom.to_monoid_hom

theorem ennreal.smul_def {M : Type u_1} [mul_action ℝ≥0∞ M] (c : ℝ≥0) (x : M) :

c • x = ↑c • x

@[protected, instance]

def ennreal.is_scalar_tower {M : Type u_1} {N : Type u_2} [mul_action ℝ≥0∞ M] [mul_action ℝ≥0∞ N] [has_scalar M N] [is_scalar_tower ℝ≥0∞ M N] :

is_scalar_tower ℝ≥0 M N

@[protected, instance]

def ennreal.smul_comm_class_left {M : Type u_1} {N : Type u_2} [mul_action ℝ≥0∞ N] [has_scalar M N] [smul_comm_class ℝ≥0∞ M N] :

smul_comm_class ℝ≥0 M N

@[protected, instance]

def ennreal.smul_comm_class_right {M : Type u_1} {N : Type u_2} [mul_action ℝ≥0∞ N] [has_scalar M N] [smul_comm_class M ℝ≥0∞ N] :

smul_comm_class M ℝ≥0 N

@[protected, instance]

noncomputable def ennreal.distrib_mul_action {M : Type u_1} [add_monoid M] [distrib_mul_action ℝ≥0∞ M] :

distrib_mul_action ℝ≥0 M

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

Equations

ennreal.distrib_mul_action = distrib_mul_action.comp_hom M ennreal.of_nnreal_hom.to_monoid_hom

@[protected, instance]

noncomputable def ennreal.module {M : Type u_1} [add_comm_monoid M] [module ℝ≥0∞ M] :

module ℝ≥0 M

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

Equations

ennreal.module = module.comp_hom M ennreal.of_nnreal_hom

@[protected, instance]

noncomputable def ennreal.algebra {A : Type u_1} [semiring A] [algebra ℝ≥0∞ A] :

algebra ℝ≥0 A

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

Equations

ennreal.algebra = {to_has_scalar := {smul := has_scalar.smul smul_with_zero.to_has_scalar}, to_ring_hom := (algebra_map ℝ≥0∞ A).comp ennreal.of_nnreal_hom, commutes' := _, smul_def' := _}

theorem ennreal.coe_smul {R : Type u_1} (r : R) (s : ℝ≥0) [has_scalar R ℝ≥0] [has_scalar R ℝ≥0∞] [is_scalar_tower R ℝ≥0 ℝ≥0] [is_scalar_tower R ℝ≥0 ℝ≥0∞] :

↑(r • s) = r • ↑s

@[simp, norm_cast]

theorem ennreal.coe_indicator {α : Type u_1} (s : set α) (f : α → ℝ≥0) (a : α) :

↑(s.indicator f a) = s.indicator (λ (x : α), ↑(f x)) a

@[simp, norm_cast]

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.not_lt_top {x : ℝ≥0∞} :

¬x < ⊤ ↔ x = ⊤

theorem ennreal.add_ne_top {a b : ℝ≥0∞} :

a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤

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.lt_top_of_mul_ne_top_left {a b : ℝ≥0∞} (h : a * b ≠ ⊤) (hb : b ≠ 0) :

theorem ennreal.lt_top_of_mul_ne_top_right {a b : ℝ≥0∞} (h : a * b ≠ ⊤) (ha : a ≠ 0) :

theorem ennreal.mul_lt_top_iff {a b : ℝ≥0∞} :

a * b < ⊤ ↔ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0

theorem ennreal.mul_self_lt_top_iff {a : ℝ≥0∞} :

a * a < ⊤ ↔ a < ⊤

theorem ennreal.mul_pos_iff {a b : ℝ≥0∞} :

0 < a * b ↔ 0 < a ∧ 0 < b

theorem ennreal.mul_pos {a b : ℝ≥0∞} (ha : a ≠ 0) (hb : b ≠ 0) :

0 < a * b

@[simp]

theorem ennreal.pow_eq_top_iff {a : ℝ≥0∞} {n : ℕ} :

a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0

theorem ennreal.pow_eq_top {a : ℝ≥0∞} (n : ℕ) (h : a ^ n = ⊤) :

theorem ennreal.pow_ne_top {a : ℝ≥0∞} (h : a ≠ ⊤) {n : ℕ} :

theorem ennreal.pow_lt_top {a : ℝ≥0∞} :

a < ⊤ → ∀ (n : ℕ), a ^ n < ⊤

@[simp, norm_cast]

theorem ennreal.coe_finset_sum {α : Type u_1} {s : finset α} {f : α → ℝ≥0} :

↑∑ (a : α) in s, f a = ∑ (a : α) in s, ↑(f a)

@[simp, norm_cast]

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 :

@[simp]

theorem ennreal.coe_lt_top {r : ℝ≥0} :

@[simp]

theorem ennreal.not_top_le_coe {r : ℝ≥0} :

@[simp, norm_cast]

theorem ennreal.one_le_coe_iff {r : ℝ≥0} :

1 ≤ ↑r ↔ 1 ≤ r

@[simp, norm_cast]

theorem ennreal.coe_le_one_iff {r : ℝ≥0} :

↑r ≤ 1 ↔ r ≤ 1

@[simp, norm_cast]

theorem ennreal.coe_lt_one_iff {p : ℝ≥0} :

↑p < 1 ↔ p < 1

@[simp, norm_cast]

theorem ennreal.one_lt_coe_iff {p : ℝ≥0} :

1 < ↑p ↔ 1 < p

@[simp, norm_cast]

theorem ennreal.coe_nat (n : ℕ) :

@[simp]

theorem ennreal.of_real_coe_nat (n : ℕ) :

ennreal.of_real ↑n = ↑n

@[simp]

theorem ennreal.nat_ne_top (n : ℕ) :

@[simp]

theorem ennreal.top_ne_nat (n : ℕ) :

@[simp]

theorem ennreal.one_lt_top :

@[simp, norm_cast]

theorem ennreal.to_nnreal_nat (n : ℕ) :

↑n.to_nnreal = ↑n

@[simp, norm_cast]

theorem ennreal.to_real_nat (n : ℕ) :

↑n.to_real = ↑n

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 = ↑p → r ≤ p

theorem ennreal.lt_iff_exists_coe {a b : ℝ≥0∞} :

a < b ↔ ∃ (p : ℝ≥0), a = ↑p ∧ ↑p < b

theorem ennreal.to_real_le_coe_of_le_coe {a : ℝ≥0∞} {b : ℝ≥0} (h : a ≤ ↑b) :

a.to_real ≤ ↑b

@[simp, norm_cast]

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

theorem ennreal.one_le_pow_of_one_le {a : ℝ≥0∞} (ha : 1 ≤ a) (n : ℕ) :

1 ≤ a ^ n

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

@[protected]

theorem ennreal.pow_pos {a : ℝ≥0∞} :

0 < a → ∀ (n : ℕ), 0 < a ^ n

@[protected]

theorem ennreal.pow_ne_zero {a : ℝ≥0∞} :

a ≠ 0 → ∀ (n : ℕ), a ^ n ≠ 0

@[simp]

theorem ennreal.not_lt_zero {a : ℝ≥0∞} :

¬a < 0

@[protected]

theorem ennreal.le_of_add_le_add_left {a b c : ℝ≥0∞} :

a ≠ ⊤ → a + b ≤ a + c → b ≤ c

@[protected]

theorem ennreal.le_of_add_le_add_right {a b c : ℝ≥0∞} :

a ≠ ⊤ → b + a ≤ c + a → b ≤ c

@[protected]

theorem ennreal.add_lt_add_left {a b c : ℝ≥0∞} :

a ≠ ⊤ → b < c → a + b < a + c

@[protected]

theorem ennreal.add_lt_add_right {a b c : ℝ≥0∞} :

a ≠ ⊤ → b < c → b + a < c + a

@[protected]

theorem ennreal.add_le_add_iff_left {a b c : ℝ≥0∞} :

a ≠ ⊤ → (a + b ≤ a + c ↔ b ≤ c)

@[protected]

theorem ennreal.add_le_add_iff_right {a b c : ℝ≥0∞} :

a ≠ ⊤ → (b + a ≤ c + a ↔ b ≤ c)

@[protected]

theorem ennreal.add_lt_add_iff_left {a b c : ℝ≥0∞} :

a ≠ ⊤ → (a + b < a + c ↔ b < c)

@[protected]

theorem ennreal.add_lt_add_iff_right {a b c : ℝ≥0∞} :

a ≠ ⊤ → (b + a < c + a ↔ b < c)

@[protected]

theorem ennreal.add_lt_add_of_le_of_lt {a b c d : ℝ≥0∞} :

a ≠ ⊤ → a ≤ b → c < d → a + c < b + d

@[protected]

theorem ennreal.add_lt_add_of_lt_of_le {a b c d : ℝ≥0∞} :

c ≠ ⊤ → a < b → c ≤ d → a + c < b + d

@[protected, instance]

def ennreal.contravariant_class_add_lt :

contravariant_class ℝ≥0∞ ℝ≥0∞ has_add.add has_lt.lt

theorem ennreal.lt_add_right {a b : ℝ≥0∞} (ha : a ≠ ⊤) (hb : b ≠ 0) :

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 ∧ a < ennreal.of_real r ∧ ennreal.of_real r < b

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, norm_cast]

theorem ennreal.coe_nat_lt_coe_nat {m n : ℕ} :

↑m < ↑n ↔ m < n

theorem ennreal.coe_nat_ne_top {n : ℕ} :

theorem ennreal.coe_nat_mono :

strict_mono coe

@[simp, norm_cast]

theorem ennreal.coe_nat_le_coe_nat {m n : ℕ} :

↑m ≤ ↑n ↔ m ≤ n

@[protected, instance]

def ennreal.char_zero :

char_zero ℝ≥0∞

@[protected]

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

@[norm_cast]

theorem ennreal.coe_min {r p : ℝ≥0} :

↑(min r p) = min ↑r ↑p

@[norm_cast]

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.to_nnreal ≤ b.to_nnreal) :

a ≤ b

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)

@[simp]

theorem ennreal.top_mem_upper_bounds {s : set ℝ≥0∞} :

⊤ ∈ upper_bounds s

theorem ennreal.coe_mem_upper_bounds {r : ℝ≥0} {s : set ℝ≥0} :

↑r ∈ upper_bounds (coe '' s) ↔ r ∈ upper_bounds s

theorem ennreal.mul_le_mul {a b c d : ℝ≥0∞} :

a ≤ b → c ≤ d → a * 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_left_mono {a : ℝ≥0∞} :

monotone (has_mul.mul a)

theorem ennreal.mul_right_mono {a : ℝ≥0∞} :

monotone (λ (x : ℝ≥0∞), x * a)

theorem ennreal.pow_strict_mono {n : ℕ} (hn : n ≠ 0) :

strict_mono (λ (x : ℝ≥0∞), x ^ n)

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 ≠ 0 → a ≠ ⊤ → (a * b = a * c ↔ b = c)

theorem ennreal.mul_eq_mul_right {a b c : ℝ≥0∞} :

c ≠ 0 → c ≠ ⊤ → (a * c = b * c ↔ a = b)

theorem ennreal.mul_le_mul_left {a b c : ℝ≥0∞} :

a ≠ 0 → a ≠ ⊤ → (a * b ≤ a * c ↔ b ≤ c)

theorem ennreal.mul_le_mul_right {a b c : ℝ≥0∞} :

c ≠ 0 → c ≠ ⊤ → (a * c ≤ b * c ↔ a ≤ b)

theorem ennreal.mul_lt_mul_left {a b c : ℝ≥0∞} :

a ≠ 0 → a ≠ ⊤ → (a * b < a * c ↔ b < c)

theorem ennreal.mul_lt_mul_right {a b c : ℝ≥0∞} :

c ≠ 0 → c ≠ ⊤ → (a * c < b * c ↔ a < b)

theorem ennreal.add_le_cancellable_iff_ne {a : ℝ≥0∞} :

add_le_cancellable a ↔ a ≠ ⊤

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 : ℝ≥0∞} (h : a ≠ ⊤) :

add_le_cancellable a

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

theorem ennreal.cancel_of_lt {a : ℝ≥0∞} (h : a < ⊤) :

add_le_cancellable a

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

theorem ennreal.cancel_of_lt' {a b : ℝ≥0∞} (h : a < b) :

add_le_cancellable a

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

theorem ennreal.cancel_coe {a : ℝ≥0} :

add_le_cancellable ↑a

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

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

theorem ennreal.sub_eq_Inf {a b : ℝ≥0∞} :

a - b = Inf {d : ℝ≥0∞ | a ≤ d + b}

theorem ennreal.coe_sub {r p : ℝ≥0} :

↑(r - p) = ↑r - ↑p

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

theorem ennreal.top_sub_coe {r : ℝ≥0} :

⊤ - ↑r = ⊤

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

theorem ennreal.sub_top {a : ℝ≥0∞} :

a - ⊤ = 0

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

theorem ennreal.sub_eq_top_iff {a b : ℝ≥0∞} :

a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤

theorem ennreal.sub_ne_top {a b : ℝ≥0∞} (ha : a ≠ ⊤) :

@[protected]

theorem ennreal.sub_lt_of_lt_add {a b c : ℝ≥0∞} (hac : c ≤ a) (h : a < b + c) :

a - c < b

@[simp]

theorem ennreal.add_sub_self {a b : ℝ≥0∞} (hb : b ≠ ⊤) :

a + b - b = a

@[simp]

theorem ennreal.add_sub_self' {a b : ℝ≥0∞} (ha : a ≠ ⊤) :

a + b - a = b

theorem ennreal.sub_eq_of_add_eq {a b c : ℝ≥0∞} (hb : b ≠ ⊤) (hc : a + b = c) :

c - b = a

@[protected]

theorem ennreal.lt_add_of_sub_lt {a b c : ℝ≥0∞} (ht : a ≠ ⊤ ∨ b ≠ ⊤) (h : a - b < c) :

a < c + b

@[protected]

theorem ennreal.sub_lt_iff_lt_add {a b c : ℝ≥0∞} (hb : b ≠ ⊤) (hab : b ≤ a) :

a - b < c ↔ a < c + b

@[protected]

theorem ennreal.sub_lt_self {a b : ℝ≥0∞} (hat : a ≠ ⊤) (ha0 : a ≠ 0) (hb : b ≠ 0) :

a - b < a

theorem ennreal.sub_lt_of_sub_lt {a b c : ℝ≥0∞} (h₂ : c ≤ a) (h₃ : a ≠ ⊤ ∨ b ≠ ⊤) (h₁ : a - b < c) :

a - c < b

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 < b → b < a → c ≠ ⊤) :

(a - b) * c = a * c - b * c

theorem ennreal.mul_sub {a b c : ℝ≥0∞} (h : 0 < c → c < b → a ≠ ⊤) :

a * (b - c) = a * b - a * c

theorem ennreal.prod_lt_top {α : Type u_1} {s : finset α} {f : α → ℝ≥0∞} (h : ∀ (a : α), a ∈ s → f 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∞} (h : ∀ (a : α), a ∈ s → f 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 ∈ s → f 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.lt_top_of_sum_ne_top {α : Type u_1} {s : finset α} {f : α → ℝ≥0∞} (h : ∑ (x : α) in s, f x ≠ ⊤) {a : α} (ha : a ∈ s) :

f a < ⊤

theorem ennreal.to_nnreal_sum {α : Type u_1} {s : finset α} {f : α → ℝ≥0∞} (hf : ∀ (a : α), a ∈ s → f 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 ∈ s → f 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 ∈ s → 0 ≤ f i) :

ennreal.of_real (∑ (i : α) in s, f i) = ∑ (i : α) in s, ennreal.of_real (f i)

theorem ennreal.sum_lt_sum_of_nonempty {α : Type u_1} {s : finset α} (hs : s.nonempty) {f g : α → ℝ≥0∞} (Hlt : ∀ (i : α), i ∈ s → f i < g i) :

∑ (i : α) in s, f i < ∑ (i : α) in s, g i

theorem ennreal.exists_le_of_sum_le {α : Type u_1} {s : finset α} (hs : s.nonempty) {f g : α → ℝ≥0∞} (Hle : ∑ (i : α) in s, f i ≤ ∑ (i : α) in s, g i) :

∃ (i : α) (H : i ∈ s), f i ≤ g i

@[protected]

theorem ennreal.Ico_eq_Iio {y : ℝ≥0∞} :

set.Ico 0 y = set.Iio y

theorem ennreal.mem_Iio_self_add {x ε : ℝ≥0∞} :

x ≠ ⊤ → ε ≠ 0 → x ∈ set.Iio (x + ε)

theorem ennreal.mem_Ioo_self_sub_add {x ε₁ ε₂ : ℝ≥0∞} :

x ≠ ⊤ → x ≠ 0 → ε₁ ≠ 0 → ε₂ ≠ 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]

theorem ennreal.bit0_eq_top_iff {a : ℝ≥0∞} :

bit0 a = ⊤ ↔ a = ⊤

@[simp]

theorem ennreal.bit1_inj {a b : ℝ≥0∞} :

bit1 a = bit1 b ↔ a = b

@[simp]

theorem ennreal.bit1_ne_zero {a : ℝ≥0∞} :

@[simp]

theorem ennreal.bit1_eq_one_iff {a : ℝ≥0∞} :

bit1 a = 1 ↔ a = 0

@[simp]

theorem ennreal.bit1_eq_top_iff {a : ℝ≥0∞} :

bit1 a = ⊤ ↔ a = ⊤

@[protected, instance]

noncomputable def ennreal.has_inv :

has_inv ℝ≥0∞

Equations

ennreal.has_inv = {inv := λ (a : ℝ≥0∞), Inf {b : ℝ≥0∞ | 1 ≤ a * b}}

@[protected, instance]

noncomputable def ennreal.div_inv_monoid :

div_inv_monoid ℝ≥0∞

Equations

ennreal.div_inv_monoid = {mul := monoid.mul infer_instance, mul_assoc := ennreal.div_inv_monoid._proof_1, one := monoid.one infer_instance, one_mul := ennreal.div_inv_monoid._proof_2, mul_one := ennreal.div_inv_monoid._proof_3, npow := monoid.npow infer_instance, npow_zero' := ennreal.div_inv_monoid._proof_4, npow_succ' := ennreal.div_inv_monoid._proof_5, inv := has_inv.inv ennreal.has_inv, div := λ (a b : ℝ≥0∞), monoid.mul a b⁻¹, div_eq_mul_inv := ennreal.div_inv_monoid._proof_6, zpow := zpow_rec {inv := has_inv.inv ennreal.has_inv}, zpow_zero' := ennreal.div_inv_monoid._proof_12, zpow_succ' := ennreal.div_inv_monoid._proof_13, zpow_neg' := ennreal.div_inv_monoid._proof_14}

@[simp]

theorem ennreal.inv_zero :

@[simp]

theorem ennreal.inv_top :

@[simp, norm_cast]

theorem ennreal.coe_inv {r : ℝ≥0} (hr : r ≠ 0) :

↑r⁻¹ = (↑r)⁻¹

theorem ennreal.coe_inv_le {r : ℝ≥0} :

↑r⁻¹ ≤ (↑r)⁻¹

@[norm_cast]

theorem ennreal.coe_inv_two :

↑2⁻¹ = 2⁻¹

@[simp, norm_cast]

theorem ennreal.coe_div {r p : ℝ≥0} (hr : r ≠ 0) :

↑(p / r) = ↑p / ↑r

theorem ennreal.div_zero {a : ℝ≥0∞} (h : a ≠ 0) :

a / 0 = ⊤

@[simp]

theorem ennreal.inv_one :

@[simp]

theorem ennreal.div_one {a : ℝ≥0∞} :

a / 1 = a

@[protected]

theorem ennreal.inv_pow {a : ℝ≥0∞} {n : ℕ} :

(a ^ n)⁻¹ = a⁻¹ ^ n

@[protected, instance]

noncomputable def ennreal.has_involutive_inv :

has_involutive_inv ℝ≥0∞

Equations

ennreal.has_involutive_inv = {inv := has_inv.inv ennreal.has_inv, inv_inv := ennreal.has_involutive_inv._proof_1}

@[simp]

theorem ennreal.inv_eq_top {a : ℝ≥0∞} :

a⁻¹ = ⊤ ↔ a = 0

theorem ennreal.inv_ne_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 : y ≠ 0) :

x / y < ⊤

@[simp]

theorem ennreal.inv_eq_zero {a : ℝ≥0∞} :

a⁻¹ = 0 ↔ a = ⊤

theorem ennreal.inv_ne_zero {a : ℝ≥0∞} :

a⁻¹ ≠ 0 ↔ a ≠ ⊤

theorem ennreal.mul_inv {a b : ℝ≥0∞} (ha : a ≠ 0 ∨ b ≠ ⊤) (hb : a ≠ ⊤ ∨ b ≠ 0) :

(a * b)⁻¹ = a⁻¹ * b⁻¹

@[simp]

theorem ennreal.inv_pos {a : ℝ≥0∞} :

0 < a⁻¹ ↔ a ≠ ⊤

@[simp]

theorem ennreal.inv_lt_inv {a b : ℝ≥0∞} :

a⁻¹ < b⁻¹ ↔ b < a

theorem ennreal.inv_lt_iff_inv_lt {a b : ℝ≥0∞} :

a⁻¹ < b ↔ b⁻¹ < a

theorem ennreal.lt_inv_iff_lt_inv {a b : ℝ≥0∞} :

a < b⁻¹ ↔ b < a⁻¹

@[simp]

theorem ennreal.inv_le_inv {a b : ℝ≥0∞} :

a⁻¹ ≤ b⁻¹ ↔ b ≤ a

theorem ennreal.inv_le_iff_inv_le {a b : ℝ≥0∞} :

a⁻¹ ≤ b ↔ b⁻¹ ≤ a

theorem ennreal.le_inv_iff_le_inv {a b : ℝ≥0∞} :

a ≤ b⁻¹ ↔ b ≤ a⁻¹

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

noncomputable def order_iso.inv_ennreal :

ℝ≥0∞ ≃o order_dual ℝ≥0∞

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

Equations

order_iso.inv_ennreal = {to_equiv := {to_fun := λ (x : ℝ≥0∞), x⁻¹, inv_fun := λ (x : order_dual ℝ≥0∞), x⁻¹, left_inv := order_iso.inv_ennreal._proof_1, right_inv := order_iso.inv_ennreal._proof_2}, map_rel_iff' := order_iso.inv_ennreal._proof_3}

@[simp]

theorem order_iso.inv_ennreal_apply (x : ℝ≥0∞) :

⇑order_iso.inv_ennreal x = x⁻¹

@[simp]

theorem order_iso.inv_ennreal_symm_apply {a : ℝ≥0∞} :

⇑(order_iso.inv_ennreal.symm) a = 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} :

⊤ / ↑p = ⊤

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.lt_div_iff_mul_lt {a b c : ℝ≥0∞} (hb0 : b ≠ 0 ∨ c ≠ ⊤) (hbt : b ≠ ⊤ ∨ c ≠ 0) :

c < a / b ↔ c * b < a

theorem ennreal.div_le_of_le_mul {a b c : ℝ≥0∞} (h : a ≤ b * c) :

a / c ≤ b

theorem ennreal.div_le_of_le_mul' {a b c : ℝ≥0∞} (h : a ≤ b * c) :

a / b ≤ c

theorem ennreal.mul_le_of_le_div {a b c : ℝ≥0∞} (h : a ≤ b / c) :

a * c ≤ b

theorem ennreal.mul_le_of_le_div' {a b c : ℝ≥0∞} (h : a ≤ b / c) :

c * a ≤ b

@[protected]

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.mul_lt_of_lt_div' {a b c : ℝ≥0∞} (h : a < b / c) :

c * a < 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) :

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 < x → ↑r ≤ y) :

x ≤ y

theorem ennreal.le_of_forall_pos_nnreal_lt {x y : ℝ≥0∞} (h : ∀ (r : ℝ≥0), 0 < r → ↑r < x → ↑r ≤ y) :

x ≤ y

theorem ennreal.eq_top_of_forall_nnreal_le {x : ℝ≥0∞} (h : ∀ (r : ℝ≥0), ↑r ≤ x) :

theorem ennreal.add_div {a b c : ℝ≥0∞} :

(a + b) / c = a / c + b / c

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.inv_two_add_inv_two :

2⁻¹ + 2⁻¹ = 1

theorem ennreal.inv_three_add_inv_three :

3⁻¹ + 3⁻¹ + 3⁻¹ = 1

@[simp]

theorem ennreal.add_halves (a : ℝ≥0∞) :

a / 2 + a / 2 = a

@[simp]

theorem ennreal.add_thirds (a : ℝ≥0∞) :

a / 3 + a / 3 + a / 3 = 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 : a ≠ 0) :

0 < a / 2

theorem ennreal.one_half_lt_one :

theorem ennreal.half_lt_self {a : ℝ≥0∞} (hz : a ≠ 0) (ht : a ≠ ⊤) :

a / 2 < a

theorem ennreal.half_le_self {a : ℝ≥0∞} :

a / 2 ≤ a

theorem ennreal.sub_half {a : ℝ≥0∞} (h : a ≠ ⊤) :

a - a / 2 = a / 2

@[simp]

theorem ennreal.one_sub_inv_two :

1 - 2⁻¹ = 2⁻¹

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

@[simp, norm_cast]

theorem ennreal.coe_zpow {r : ℝ≥0} (hr : r ≠ 0) (n : ℤ) :

↑(r ^ n) = ↑r ^ n

theorem ennreal.zpow_pos {a : ℝ≥0∞} (ha : a ≠ 0) (h'a : a ≠ ⊤) (n : ℤ) :

0 < a ^ n

theorem ennreal.zpow_lt_top {a : ℝ≥0∞} (ha : a ≠ 0) (h'a : a ≠ ⊤) (n : ℤ) :

a ^ n < ⊤

theorem ennreal.exists_mem_Ico_zpow {x y : ℝ≥0∞} (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 : ℝ≥0∞} (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 : ℝ≥0∞} (hy : 1 < y) (h'y : y ≠ ⊤) :

set.Ioo 0 ⊤ = ⋃ (n : ℤ), set.Ico (y ^ n) (y ^ (n + 1))

theorem ennreal.zpow_le_of_le {x : ℝ≥0∞} (hx : 1 ≤ x) {a b : ℤ} (h : a ≤ b) :

x ^ a ≤ x ^ b

theorem ennreal.monotone_zpow {x : ℝ≥0∞} (hx : 1 ≤ x) :

monotone (pow x)

theorem ennreal.zpow_add {x : ℝ≥0∞} (hx : x ≠ 0) (h'x : x ≠ ⊤) (m n : ℤ) :

x ^ (m + n) = (x ^ m) * x ^ n

theorem ennreal.to_real_add {a b : ℝ≥0∞} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

(a + b).to_real = a.to_real + b.to_real

theorem ennreal.to_real_sub_of_le {a b : ℝ≥0∞} (h : b ≤ a) (ha : a ≠ ⊤) :

(a - b).to_real = a.to_real - b.to_real

theorem ennreal.le_to_real_sub {a b : ℝ≥0∞} (hb : b ≠ ⊤) :

a.to_real - b.to_real ≤ (a - b).to_real

theorem ennreal.to_real_add_le {a b : ℝ≥0∞} :

(a + b).to_real ≤ a.to_real + b.to_real

theorem ennreal.of_real_add {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) :

ennreal.of_real (p + q) = ennreal.of_real p + ennreal.of_real q

theorem ennreal.of_real_add_le {p q : ℝ} :

ennreal.of_real (p + q) ≤ ennreal.of_real p + ennreal.of_real q

@[simp]

theorem ennreal.to_real_le_to_real {a b : ℝ≥0∞} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

a.to_real ≤ b.to_real ↔ a ≤ b

theorem ennreal.to_real_mono {a b : ℝ≥0∞} (hb : b ≠ ⊤) (h : a ≤ b) :

a.to_real ≤ b.to_real

@[simp]

theorem ennreal.to_real_lt_to_real {a b : ℝ≥0∞} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

a.to_real < b.to_real ↔ a < b

theorem ennreal.to_real_strict_mono {a b : ℝ≥0∞} (hb : b ≠ ⊤) (h : a < b) :

a.to_real < b.to_real

theorem ennreal.to_nnreal_mono {a b : ℝ≥0∞} (hb : b ≠ ⊤) (h : a ≤ b) :

a.to_nnreal ≤ b.to_nnreal

@[simp]

theorem ennreal.to_nnreal_le_to_nnreal {a b : ℝ≥0∞} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

a.to_nnreal ≤ b.to_nnreal ↔ a ≤ b

theorem ennreal.to_nnreal_strict_mono {a b : ℝ≥0∞} (hb : b ≠ ⊤) (h : a < b) :

a.to_nnreal < b.to_nnreal

@[simp]

theorem ennreal.to_nnreal_lt_to_nnreal {a b : ℝ≥0∞} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

a.to_nnreal < b.to_nnreal ↔ a < b

theorem ennreal.to_real_max {a b : ℝ≥0∞} (hr : a ≠ ⊤) (hp : b ≠ ⊤) :

(max a b).to_real = max a.to_real b.to_real

theorem ennreal.to_nnreal_pos_iff {a : ℝ≥0∞} :

0 < a.to_nnreal ↔ 0 < a ∧ a < ⊤

theorem ennreal.to_nnreal_pos {a : ℝ≥0∞} (ha₀ : a ≠ 0) (ha_top : a ≠ ⊤) :

0 < a.to_nnreal

theorem ennreal.to_real_pos_iff {a : ℝ≥0∞} :

0 < a.to_real ↔ 0 < a ∧ a < ⊤

theorem ennreal.to_real_pos {a : ℝ≥0∞} (ha₀ : a ≠ 0) (ha_top : a ≠ ⊤) :

theorem ennreal.of_real_le_of_real {p q : ℝ} (h : p ≤ q) :

ennreal.of_real p ≤ ennreal.of_real q

theorem ennreal.of_real_le_of_le_to_real {a : ℝ} {b : ℝ≥0∞} (h : a ≤ b.to_real) :

ennreal.of_real a ≤ b

@[simp]

theorem ennreal.of_real_le_of_real_iff {p q : ℝ} (h : 0 ≤ q) :

ennreal.of_real p ≤ ennreal.of_real q ↔ p ≤ q

@[simp]

theorem ennreal.of_real_lt_of_real_iff {p q : ℝ} (h : 0 < q) :

ennreal.of_real p < ennreal.of_real q ↔ p < q

theorem ennreal.of_real_lt_of_real_iff_of_nonneg {p q : ℝ} (hp : 0 ≤ p) :

ennreal.of_real p < ennreal.of_real q ↔ p < q

@[simp]

theorem ennreal.of_real_pos {p : ℝ} :

0 < ennreal.of_real p ↔ 0 < p

@[simp]

theorem ennreal.of_real_eq_zero {p : ℝ} :

ennreal.of_real p = 0 ↔ p ≤ 0

@[simp]

theorem ennreal.zero_eq_of_real {p : ℝ} :

0 = ennreal.of_real p ↔ p ≤ 0

theorem ennreal.of_real_le_iff_le_to_real {a : ℝ} {b : ℝ≥0∞} (hb : b ≠ ⊤) :

ennreal.of_real a ≤ b ↔ a ≤ b.to_real

theorem ennreal.of_real_lt_iff_lt_to_real {a : ℝ} {b : ℝ≥0∞} (ha : 0 ≤ a) (hb : b ≠ ⊤) :

ennreal.of_real a < b ↔ a < b.to_real

theorem ennreal.le_of_real_iff_to_real_le {a : ℝ≥0∞} {b : ℝ} (ha : a ≠ ⊤) (hb : 0 ≤ b) :

a ≤ ennreal.of_real b ↔ a.to_real ≤ b

theorem ennreal.to_real_le_of_le_of_real {a : ℝ≥0∞} {b : ℝ} (hb : 0 ≤ b) (h : a ≤ ennreal.of_real b) :

a.to_real ≤ b

theorem ennreal.lt_of_real_iff_to_real_lt {a : ℝ≥0∞} {b : ℝ} (ha : a ≠ ⊤) :

a < ennreal.of_real b ↔ a.to_real < b

theorem ennreal.of_real_mul {p q : ℝ} (hp : 0 ≤ p) :

ennreal.of_real (p * q) = (ennreal.of_real p) * ennreal.of_real q

theorem ennreal.of_real_pow {p : ℝ} (hp : 0 ≤ p) (n : ℕ) :

ennreal.of_real (p ^ n) = ennreal.of_real p ^ n

theorem ennreal.of_real_inv_of_pos {x : ℝ} (hx : 0 < x) :

(ennreal.of_real x)⁻¹ = ennreal.of_real x⁻¹

theorem ennreal.of_real_div_of_pos {x y : ℝ} (hy : 0 < y) :

ennreal.of_real (x / y) = ennreal.of_real x / ennreal.of_real y

theorem ennreal.to_real_of_real_mul (c : ℝ) (a : ℝ≥0∞) (h : 0 ≤ c) :

((ennreal.of_real c) * a).to_real = c * a.to_real

@[simp]

theorem ennreal.to_nnreal_mul_top (a : ℝ≥0∞) :

(a * ⊤).to_nnreal = 0

@[simp]

theorem ennreal.to_nnreal_top_mul (a : ℝ≥0∞) :

(⊤ * a).to_nnreal = 0

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

a.to_real = b.to_real ↔ a = b

theorem ennreal.to_real_smul (r : ℝ≥0) (s : ℝ≥0∞) :

(r • s).to_real = r • s.to_real

@[protected]

theorem ennreal.trichotomy (p : ℝ≥0∞) :

p = 0 ∨ p = ⊤ ∨ 0 < p.to_real

@[protected]

theorem ennreal.trichotomy₂ {p q : ℝ≥0∞} (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 : ℝ≥0∞) [fact (1 ≤ p)] :

p = ⊤ ∨ 1 ≤ p.to_real

def ennreal.to_nnreal_hom :

ℝ≥0∞ →* ℝ≥0

ennreal.to_nnreal as a monoid_hom.

Equations

ennreal.to_nnreal_hom = {to_fun := ennreal.to_nnreal, map_one' := ennreal.to_nnreal_hom._proof_1, map_mul' := ennreal.to_nnreal_hom._proof_2}

theorem ennreal.to_nnreal_mul {a b : ℝ≥0∞} :

(a * b).to_nnreal = (a.to_nnreal) * b.to_nnreal

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

theorem ennreal.to_nnreal_inv (a : ℝ≥0∞) :

a⁻¹.to_nnreal = (a.to_nnreal)⁻¹

theorem ennreal.to_nnreal_div (a b : ℝ≥0∞) :

(a / b).to_nnreal = a.to_nnreal / b.to_nnreal

noncomputable def ennreal.to_real_hom :

ℝ≥0∞ →* ℝ

ennreal.to_real as a monoid_hom.

Equations

ennreal.to_real_hom = ↑nnreal.to_real_hom.comp ennreal.to_nnreal_hom

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.to_real_inv (a : ℝ≥0∞) :

a⁻¹.to_real = (a.to_real)⁻¹

theorem ennreal.to_real_div (a b : ℝ≥0∞) :

(a / b).to_real = a.to_real / b.to_real

theorem ennreal.of_real_prod_of_nonneg {α : Type u_1} {s : finset α} {f : α → ℝ} (hf : ∀ (i : α), i ∈ s → 0 ≤ f i) :

ennreal.of_real (∏ (i : α) in s, f i) = ∏ (i : α) in s, ennreal.of_real (f i)

@[simp]

theorem ennreal.to_nnreal_bit0 {x : ℝ≥0∞} :

(bit0 x).to_nnreal = bit0 x.to_nnreal

@[simp]

theorem ennreal.to_nnreal_bit1 {x : ℝ≥0∞} (hx_top : x ≠ ⊤) :

(bit1 x).to_nnreal = bit1 x.to_nnreal

@[simp]

theorem ennreal.to_real_bit0 {x : ℝ≥0∞} :

(bit0 x).to_real = bit0 x.to_real

@[simp]

theorem ennreal.to_real_bit1 {x : ℝ≥0∞} (hx_top : x ≠ ⊤) :

(bit1 x).to_real = bit1 x.to_real

@[simp]

theorem ennreal.of_real_bit0 {r : ℝ} (hr : 0 ≤ r) :

ennreal.of_real (bit0 r) = bit0 (ennreal.of_real r)

@[simp]

theorem ennreal.of_real_bit1 {r : ℝ} (hr : 0 ≤ r) :

ennreal.of_real (bit1 r) = bit1 (ennreal.of_real 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 ∈ t → f 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) = ⊤