Properties of addition, multiplication and subtraction on extended non-negative real numbers

In this file we prove elementary properties of algebraic operations on ℝ≥0∞, including addition, multiplication, natural powers and truncated subtraction, as well as how these interact with the order structure on ℝ≥0∞. Notably excluded from this list are inversion and division, the definitions and properties of which can be found in Mathlib.Data.ENNReal.Inv.

Note: the definitions of the operations included in this file can be found in Mathlib.Data.ENNReal.Basic.

theorem ENNReal.mul_lt_mul {a b c d : ENNReal} (ac : a < c) (bd : b < d) : a * b < c * d

@[deprecated mul_left_mono (since := "2024-10-15")]

theorem ENNReal.mul_left_mono {a : ENNReal} : Monotone fun (x : ENNReal) => a * x

@[deprecated mul_right_mono (since := "2024-10-15")]

theorem ENNReal.mul_right_mono {a : ENNReal} : Monotone fun (x : ENNReal) => x * a

theorem ENNReal.pow_right_strictMono {n : ℕ} (hn : n ≠ 0) : StrictMono fun (a : ENNReal) => a ^ n

@[deprecated ENNReal.pow_right_strictMono (since := "2024-10-15")]

theorem ENNReal.pow_strictMono {n : ℕ} (hn : n ≠ 0) : StrictMono fun (a : ENNReal) => a ^ n

Alias of ENNReal.pow_right_strictMono.

theorem ENNReal.pow_lt_pow_left {a b : ENNReal} (hab : a < b) {n : ℕ} (hn : n ≠ 0) : a ^ n < b ^ n

@[deprecated max_mul (since := "2024-10-15")]

theorem ENNReal.max_mul {a b c : ENNReal} : (a ⊔ b) * c = a * c ⊔ b * c

@[deprecated mul_max (since := "2024-10-15")]

theorem ENNReal.mul_max {a b c : ENNReal} : a * (b ⊔ c) = a * b ⊔ a * c

theorem ENNReal.mul_left_strictMono {a : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) : StrictMono fun (x : ENNReal) => a * x

theorem ENNReal.mul_lt_mul_left' {a b c : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) (bc : b < c) : a * b < a * c

theorem ENNReal.mul_lt_mul_right' {a b c : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) (bc : b < c) : b * a < c * a

theorem ENNReal.mul_right_inj {a b c : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) : a * b = a * c ↔ b = c

@[deprecated ENNReal.mul_right_inj (since := "2025-01-20")]

theorem ENNReal.mul_eq_mul_left {a b c : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) : a * b = a * c ↔ b = c

Alias of ENNReal.mul_right_inj.

theorem ENNReal.mul_left_inj {a b c : ENNReal} (h0 : c ≠ 0) (hinf : c ≠ ⊤) : a * c = b * c ↔ a = b

@[deprecated ENNReal.mul_left_inj (since := "2025-01-20")]

theorem ENNReal.mul_eq_mul_right {a b c : ENNReal} (h0 : c ≠ 0) (hinf : c ≠ ⊤) : a * c = b * c ↔ a = b

Alias of ENNReal.mul_left_inj.

theorem ENNReal.mul_le_mul_left {a b c : ENNReal} (h0 : 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} (h0 : 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)

theorem ENNReal.mul_eq_left {a b : ENNReal} (ha₀ : a ≠ 0) (ha : a ≠ ⊤) : a * b = a ↔ b = 1

theorem ENNReal.mul_eq_right {a b : ENNReal} (hb₀ : b ≠ 0) (hb : b ≠ ⊤) : a * b = b ↔ a = 1

theorem ENNReal.pow_pos {a : ENNReal} : 0 < a → ∀ (n : ℕ), 0 < a ^ n

theorem ENNReal.pow_ne_zero {a : ENNReal} : a ≠ 0 → ∀ (n : ℕ), a ^ n ≠ 0

theorem ENNReal.not_lt_zero {a : ENNReal} : ¬a < 0

theorem ENNReal.le_of_add_le_add_left {a b c : ENNReal} : a ≠ ⊤ → a + b ≤ a + c → b ≤ c

theorem ENNReal.le_of_add_le_add_right {a b c : ENNReal} : a ≠ ⊤ → b + a ≤ c + a → b ≤ c

theorem ENNReal.add_lt_add_left {a b c : ENNReal} : a ≠ ⊤ → b < c → a + b < a + c

theorem ENNReal.add_lt_add_right {a b c : ENNReal} : a ≠ ⊤ → b < c → b + a < c + a

theorem ENNReal.add_le_add_iff_left {a b c : ENNReal} : a ≠ ⊤ → (a + b ≤ a + c ↔ b ≤ c)

theorem ENNReal.add_le_add_iff_right {a b c : ENNReal} : a ≠ ⊤ → (b + a ≤ c + a ↔ b ≤ c)

theorem ENNReal.add_lt_add_iff_left {a b c : ENNReal} : a ≠ ⊤ → (a + b < a + c ↔ b < c)

theorem ENNReal.add_lt_add_iff_right {a b c : ENNReal} : a ≠ ⊤ → (b + a < c + a ↔ b < c)

theorem ENNReal.add_lt_add_of_le_of_lt {a b c d : ENNReal} : a ≠ ⊤ → a ≤ b → c < d → a + c < b + d

theorem ENNReal.add_lt_add_of_lt_of_le {a b c d : ENNReal} : c ≠ ⊤ → a < b → c ≤ d → a + c < b + d

instance ENNReal.addLeftReflectLT : AddLeftReflectLT ENNReal

theorem ENNReal.lt_add_right {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ 0) : a < a + b

@[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.toNNReal_add {r₁ r₂ : ENNReal} (h₁ : r₁ ≠ ⊤) (h₂ : r₂ ≠ ⊤) : (r₁ + r₂).toNNReal = r₁.toNNReal + r₂.toNNReal

theorem ENNReal.not_lt_top {x : ENNReal} : ¬x < ⊤ ↔ x = ⊤

theorem ENNReal.add_ne_top {a b : ENNReal} : a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤

theorem ENNReal.Finiteness.add_ne_top {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a + b ≠ ⊤

theorem ENNReal.mul_top' {a : ENNReal} : a * ⊤ = if a = 0 then 0 else ⊤

@[simp]

theorem ENNReal.mul_top {a : ENNReal} (h : a ≠ 0) : a * ⊤ = ⊤

theorem ENNReal.top_mul' {a : ENNReal} : ⊤ * a = if a = 0 then 0 else ⊤

@[simp]

theorem ENNReal.top_mul {a : ENNReal} (h : a ≠ 0) : ⊤ * a = ⊤

theorem ENNReal.top_mul_top : ⊤ * ⊤ = ⊤

theorem ENNReal.top_pow {n : ℕ} (n_pos : 0 < n) : ⊤ ^ 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} : a ≠ ⊤ → b ≠ ⊤ → a * b ≠ ⊤

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_self_lt_top_iff {a : ENNReal} : a * a < ⊤ ↔ a < ⊤

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]

theorem ENNReal.coe_finset_sum {α : Type u_1} {s : Finset α} {f : α → NNReal} : ↑(∑ a ∈ s, f a) = ∑ a ∈ s, ↑(f a)

@[simp]

theorem ENNReal.coe_finset_prod {α : Type u_1} {s : Finset α} {f : α → NNReal} : ↑(∏ a ∈ s, f a) = ∏ a ∈ s, ↑(f a)

theorem ENNReal.add_lt_add {a b c d : ENNReal} (ac : a < c) (bd : b < d) : a + b < c + d

@[simp]

theorem ENNReal.addLECancellable_iff_ne {a : ENNReal} : AddLECancellable a ↔ a ≠ ⊤

An element a is AddLECancellable 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 ≠ ⊤) : AddLECancellable a

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

theorem ENNReal.cancel_of_lt {a : ENNReal} (h : a < ⊤) : AddLECancellable a

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

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

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

theorem ENNReal.cancel_coe {a : NNReal} : AddLECancellable ↑a

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_sInf {a b : ENNReal} : a - b = sInf {d : ENNReal | a ≤ d + b}

@[simp]

theorem ENNReal.coe_sub {r p : NNReal} : ↑(r - p) = ↑r - ↑p

This is a special case of WithTop.coe_sub in the ENNReal namespace

@[simp]

theorem ENNReal.top_sub_coe {r : NNReal} : ⊤ - ↑r = ⊤

This is a special case of WithTop.top_sub_coe in the ENNReal namespace

@[simp]

theorem ENNReal.top_sub {a : ENNReal} (ha : a ≠ ⊤) : ⊤ - a = ⊤

theorem ENNReal.sub_top {a : ENNReal} : a - ⊤ = 0

This is a special case of WithTop.sub_top in the ENNReal namespace

@[simp]

theorem ENNReal.sub_eq_top_iff {a b : ENNReal} : a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤

theorem ENNReal.sub_ne_top_iff {a b : ENNReal} : a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤

theorem ENNReal.sub_ne_top {a b : ENNReal} (ha : a ≠ ⊤) : a - b ≠ ⊤

@[simp]

theorem ENNReal.natCast_sub (m n : ℕ) : ↑(m - n) = ↑m - ↑n

theorem ENNReal.sub_eq_of_eq_add {a b c : ENNReal} (hb : b ≠ ⊤) : a = c + b → a - b = c

See ENNReal.sub_eq_of_eq_add' for a version assuming that a = c + b itself is finite rather than b.

theorem ENNReal.sub_eq_of_eq_add' {a b c : ENNReal} (ha : a ≠ ⊤) : a = c + b → a - b = c

Weaker version of ENNReal.sub_eq_of_eq_add assuming that a = c + b itself is finite rather han b.

theorem ENNReal.eq_sub_of_add_eq {a b c : ENNReal} (hc : c ≠ ⊤) : a + c = b → a = b - c

See ENNReal.eq_sub_of_add_eq' for a version assuming that b = a + c itself is finite rather than c.

theorem ENNReal.eq_sub_of_add_eq' {a b c : ENNReal} (hb : b ≠ ⊤) : a + c = b → a = b - c

Weaker version of ENNReal.eq_sub_of_add_eq assuming that b = a + c itself is finite rather than c.

theorem ENNReal.sub_eq_of_eq_add_rev {a b c : ENNReal} (hb : b ≠ ⊤) : a = b + c → a - b = c

See ENNReal.sub_eq_of_eq_add_rev' for a version assuming that a = b + c itself is finite rather than b.

theorem ENNReal.sub_eq_of_eq_add_rev' {a b c : ENNReal} (ha : a ≠ ⊤) : a = b + c → a - b = c

Weaker version of ENNReal.sub_eq_of_eq_add_rev assuming that a = b + c itself is finite rather than b.

@[deprecated ENNReal.sub_eq_of_eq_add (since := "2024-09-30")]

theorem ENNReal.sub_eq_of_add_eq {a b c : ENNReal} (hb : b ≠ ⊤) (hc : a + b = c) : c - b = a

@[simp]

theorem ENNReal.add_sub_cancel_left {a b : ENNReal} (ha : a ≠ ⊤) : a + b - a = b

@[simp]

theorem ENNReal.add_sub_cancel_right {a b : ENNReal} (hb : b ≠ ⊤) : a + b - b = a

theorem ENNReal.sub_add_eq_add_sub {a b c : ENNReal} (hab : b ≤ a) (b_ne_top : b ≠ ⊤) : a - b + c = a + c - b

theorem ENNReal.lt_add_of_sub_lt_left {a b c : ENNReal} (h : a ≠ ⊤ ∨ b ≠ ⊤) : a - b < c → a < b + c

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

theorem ENNReal.sub_lt_of_lt_add {a b c : ENNReal} (hac : c ≤ a) (h : a < b + c) : a - c < b

theorem ENNReal.sub_lt_iff_lt_right {a b c : ENNReal} (hb : b ≠ ⊤) (hab : b ≤ a) : a - b < c ↔ a < c + b

theorem ENNReal.sub_lt_self {a b : ENNReal} (ha : a ≠ ⊤) (ha₀ : a ≠ 0) (hb : b ≠ 0) : a - b < a

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.sub_le_sub_iff_left {a b c : ENNReal} (h : c ≤ a) (h' : a ≠ ⊤) : a - b ≤ a - c ↔ c ≤ b

theorem ENNReal.prod_ne_top {α : Type u_1} {s : Finset α} {f : α → ENNReal} (h : ∀ a ∈ s, f a ≠ ⊤) : ∏ a ∈ s, f a ≠ ⊤

A product of finite numbers is still finite.

theorem ENNReal.prod_lt_top {α : Type u_1} {s : Finset α} {f : α → ENNReal} (h : ∀ a ∈ s, f a < ⊤) : ∏ a ∈ s, f a < ⊤

A product of finite numbers is still finite.

@[simp]

theorem ENNReal.sum_eq_top {α : Type u_1} {s : Finset α} {f : α → ENNReal} : ∑ x ∈ s, f x = ⊤ ↔ ∃ a ∈ s, f a = ⊤

A sum is infinite iff one of the summands is infinite.

theorem ENNReal.sum_ne_top {α : Type u_1} {s : Finset α} {f : α → ENNReal} : ∑ a ∈ s, f a ≠ ⊤ ↔ ∀ a ∈ s, f a ≠ ⊤

A sum is finite iff all summands are finite.

@[simp]

theorem ENNReal.sum_lt_top {α : Type u_1} {s : Finset α} {f : α → ENNReal} : ∑ a ∈ s, f a < ⊤ ↔ ∀ a ∈ s, f a < ⊤

A sum is finite iff all summands are finite.

@[deprecated ENNReal.sum_lt_top (since := "2024-08-25")]

theorem ENNReal.sum_lt_top_iff {α : Type u_1} {s : Finset α} {f : α → ENNReal} : ∑ a ∈ s, f a < ⊤ ↔ ∀ a ∈ s, f a < ⊤

Alias of ENNReal.sum_lt_top.

---

A sum is finite iff all summands are finite.

theorem ENNReal.lt_top_of_sum_ne_top {α : Type u_1} {s : Finset α} {f : α → ENNReal} (h : ∑ x ∈ s, f x ≠ ⊤) {a : α} (ha : a ∈ s) : f a < ⊤

theorem ENNReal.toNNReal_sum {α : Type u_1} {s : Finset α} {f : α → ENNReal} (hf : ∀ a ∈ s, f a ≠ ⊤) : (∑ a ∈ s, f a).toNNReal = ∑ a ∈ s, (f a).toNNReal

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

theorem ENNReal.toReal_sum {α : Type u_1} {s : Finset α} {f : α → ENNReal} (hf : ∀ a ∈ s, f a ≠ ⊤) : (∑ a ∈ s, f a).toReal = ∑ a ∈ s, (f a).toReal

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

theorem ENNReal.ofReal_sum_of_nonneg {α : Type u_1} {s : Finset α} {f : α → ℝ} (hf : ∀ i ∈ s, 0 ≤ f i) : ENNReal.ofReal (∑ i ∈ s, f i) = ∑ i ∈ s, ENNReal.ofReal (f i)

theorem ENNReal.sum_lt_sum_of_nonempty {α : Type u_1} {s : Finset α} (hs : s.Nonempty) {f g : α → ENNReal} (Hlt : ∀ i ∈ s, f i < g i) : ∑ i ∈ s, f i < ∑ i ∈ s, g i

theorem ENNReal.exists_le_of_sum_le {α : Type u_1} {s : Finset α} (hs : s.Nonempty) {f g : α → ENNReal} (Hle : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i) : ∃ i ∈ s, f i ≤ g i

theorem ENNReal.Ico_eq_Iio {y : ENNReal} : Set.Ico 0 y = Set.Iio 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 + ε₂)

noncomputable instance ENNReal.instMulActionNNReal {M : Type u_1} [MulAction ENNReal M] : MulAction NNReal M

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

Equations

• ENNReal.instMulActionNNReal = MulAction.compHom M ↑ENNReal.ofNNRealHom

theorem ENNReal.smul_def {M : Type u_1} [MulAction ENNReal M] (c : NNReal) (x : M) : c • x = ↑c • x

instance ENNReal.instIsScalarTowerNNReal {M : Type u_1} {N : Type u_2} [MulAction ENNReal M] [MulAction ENNReal N] [SMul M N] [IsScalarTower ENNReal M N] : IsScalarTower NNReal M N

instance ENNReal.smulCommClass_left {M : Type u_1} {N : Type u_2} [MulAction ENNReal N] [SMul M N] [SMulCommClass ENNReal M N] : SMulCommClass NNReal M N

instance ENNReal.smulCommClass_right {M : Type u_1} {N : Type u_2} [MulAction ENNReal N] [SMul M N] [SMulCommClass M ENNReal N] : SMulCommClass M NNReal N

noncomputable instance ENNReal.instDistribMulActionNNReal {M : Type u_1} [AddMonoid M] [DistribMulAction ENNReal M] : DistribMulAction NNReal M

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

Equations

• ENNReal.instDistribMulActionNNReal = DistribMulAction.compHom M ↑ENNReal.ofNNRealHom

noncomputable instance ENNReal.instModuleNNReal {M : Type u_1} [AddCommMonoid M] [Module ENNReal M] : Module NNReal M

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

Equations

• ENNReal.instModuleNNReal = Module.compHom M ENNReal.ofNNRealHom

noncomputable instance ENNReal.instAlgebraNNReal {A : Type u_1} [Semiring A] [Algebra ENNReal A] : Algebra NNReal A

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

Equations

• ENNReal.instAlgebraNNReal = Algebra.mk ((algebraMap ENNReal A).comp ENNReal.ofNNRealHom) ⋯ ⋯

theorem ENNReal.coe_smul {R : Type u_1} (r : R) (s : NNReal) [SMul R NNReal] [SMul R ENNReal] [IsScalarTower R NNReal NNReal] [IsScalarTower R NNReal ENNReal] : ↑(r • s) = r • ↑s

theorem ENNReal.smul_top {R : Type u_1} [Zero R] [SMulWithZero R ENNReal] [IsScalarTower R ENNReal ENNReal] [NoZeroSMulDivisors R ENNReal] [DecidableEq R] (c : R) : c • ⊤ = if c = 0 then 0 else ⊤

theorem ENNReal.nnreal_smul_lt_top {x : NNReal} {y : ENNReal} (hy : y < ⊤) : x • y < ⊤

theorem ENNReal.nnreal_smul_ne_top {x : NNReal} {y : ENNReal} (hy : y ≠ ⊤) : x • y ≠ ⊤

theorem ENNReal.nnreal_smul_ne_top_iff {x : NNReal} {y : ENNReal} (hx : x ≠ 0) : x • y ≠ ⊤ ↔ y ≠ ⊤

theorem ENNReal.nnreal_smul_lt_top_iff {x : NNReal} {y : ENNReal} (hx : x ≠ 0) : x • y < ⊤ ↔ y < ⊤