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/Basic/ENNReal/Inv.lean.

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

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

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

theorem ENNReal.pow_le_pow_left_iff {a b : ENNReal} {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ b ^ n ↔ a ≤ b

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

theorem ENNReal.pow_le_pow_left {a b : ENNReal} {n : ℕ} (h : a ≤ b) : a ^ n ≤ b ^ n

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

Alias of the reverse direction of ENNReal.pow_lt_pow_left_iff.

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

theorem ENNReal.mul_right_strictMono {a : ENNReal} (h₀ : a ≠ 0) (hinf : a ≠ ⊤) : StrictMono fun (x : ENNReal) => a * x

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

theorem ENNReal.mul_lt_mul_left {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

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

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

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

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

theorem ENNReal.mul_lt_mul_iff_left {a b c : ENNReal} (h0 : c ≠ 0) (hinf : 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.toReal_le_add' {a b c : ENNReal} (hle : a ≤ b + c) (hb : b = ⊤ → a = ⊤) (hc : c = ⊤ → a = ⊤) : a.toReal ≤ b.toReal + c.toReal

If a ≤ b + c and a = ∞ whenever b = ∞ or c = ∞, then ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c. This lemma is useful to transfer triangle-like inequalities from ENNReals to Reals.

theorem ENNReal.toReal_le_add {a b c : ENNReal} (hle : a ≤ b + c) (hb : b ≠ ⊤) (hc : c ≠ ⊤) : a.toReal ≤ b.toReal + c.toReal

If a ≤ b + c, b ≠ ∞, and c ≠ ∞, then ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c. This lemma is useful to transfer triangle-like inequalities from ENNReals to Reals.

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.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.top_pow {n : ℕ} (hn : n ≠ 0) : ⊤ ^ n = ⊤

@[simp]

theorem ENNReal.pow_eq_top_iff {a : ENNReal} {n : ℕ} : a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0

theorem ENNReal.pow_ne_top_iff {a : ENNReal} {n : ℕ} : a ^ n ≠ ⊤ ↔ a ≠ ⊤ ∨ n = 0

@[simp]

theorem ENNReal.pow_lt_top_iff {a : ENNReal} {n : ℕ} : a ^ n < ⊤ ↔ a < ⊤ ∨ n = 0

theorem ENNReal.eq_top_of_pow {a : ENNReal} (n : ℕ) (ha : a ^ n = ⊤) : a = ⊤

theorem ENNReal.pow_ne_top {a : ENNReal} {n : ℕ} (ha : a ≠ ⊤) : a ^ n ≠ ⊤

theorem ENNReal.pow_lt_top {a : ENNReal} {n : ℕ} (ha : a < ⊤) : a ^ n < ⊤

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 = ⊤

@[simp]

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.

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

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.add_sub_add_eq_sub_right {a b c : ENNReal} (hc : c ≠ ⊤ := by finiteness) : a + c - (b + c) = a - b

theorem ENNReal.add_sub_add_eq_sub_left {a b c : ENNReal} (hc : c ≠ ⊤ := by finiteness) : c + a - (c + b) = a - 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_iff_lt_left {a b c : ENNReal} (hb : b ≠ ⊤) (hab : b ≤ a) : a - b < c ↔ a < b + c

theorem ENNReal.le_sub_iff_add_le_left {a b c : ENNReal} (hc : c ≠ ⊤) (hcb : c ≤ b) : a ≤ b - c ↔ c + a ≤ b

theorem ENNReal.le_sub_iff_add_le_right {a b c : ENNReal} (hc : c ≠ ⊤) (hcb : c ≤ b) : 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.le_toReal_sub {a b : ENNReal} (hb : b ≠ ⊤) : a.toReal - b.toReal ≤ (a - b).toReal

@[simp]

theorem ENNReal.toNNReal_sub {a b : ENNReal} (hb : b ≠ ⊤) : (a - b).toNNReal = a.toNNReal - b.toNNReal

@[simp]

theorem ENNReal.toReal_sub_of_le {a b : ENNReal} (hba : b ≤ a) (ha : a ≠ ⊤) : (a - b).toReal = a.toReal - b.toReal

theorem ENNReal.ofReal_sub (p : ℝ) {q : ℝ} (hq : 0 ≤ q) : ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

theorem ENNReal.sub_sub_sub_cancel_left {a b c : ENNReal} (ha : a ≠ ⊤) (h : b ≤ a) : a - c - (a - b) = b - c

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 + ε₂)

@[simp]

theorem ENNReal.image_coe_Iic (x : NNReal) : ofNNReal '' Set.Iic x = Set.Iic ↑x

@[simp]

theorem ENNReal.image_coe_Ici (x : NNReal) : ofNNReal '' Set.Ici x = Set.Ico ↑x ⊤

@[simp]

theorem ENNReal.image_coe_Iio (x : NNReal) : ofNNReal '' Set.Iio x = Set.Iio ↑x

@[simp]

theorem ENNReal.image_coe_Ioi (x : NNReal) : ofNNReal '' Set.Ioi x = Set.Ioo ↑x ⊤

@[simp]

theorem ENNReal.image_coe_Icc (x y : NNReal) : ofNNReal '' Set.Icc x y = Set.Icc ↑x ↑y

@[simp]

theorem ENNReal.image_coe_Ico (x y : NNReal) : ofNNReal '' Set.Ico x y = Set.Ico ↑x ↑y

@[simp]

theorem ENNReal.image_coe_Ioc (x y : NNReal) : ofNNReal '' Set.Ioc x y = Set.Ioc ↑x ↑y

@[simp]

theorem ENNReal.image_coe_Ioo (x y : NNReal) : ofNNReal '' Set.Ioo x y = Set.Ioo ↑x ↑y

@[simp]

theorem ENNReal.image_coe_uIcc (x y : NNReal) : ofNNReal '' Set.uIcc x y = Set.uIcc ↑x ↑y

@[simp]

theorem ENNReal.image_coe_uIoc (x y : NNReal) : ofNNReal '' Set.uIoc x y = Set.uIoc ↑x ↑y

@[simp]

theorem ENNReal.image_coe_uIoo (x y : NNReal) : ofNNReal '' Set.uIoo x y = Set.uIoo ↑x ↑y

theorem ENNReal.toNNReal_iInf {ι : Sort u_1} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) : (iInf f).toNNReal = ⨅ (i : ι), (f i).toNNReal

theorem ENNReal.toNNReal_sInf (s : Set ENNReal) (hs : ∀ r ∈ s, r ≠ ⊤) : (sInf s).toNNReal = sInf (ENNReal.toNNReal '' s)

theorem ENNReal.toReal_iInf {ι : Sort u_1} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) : (iInf f).toReal = ⨅ (i : ι), (f i).toReal

theorem ENNReal.toReal_sInf (s : Set ENNReal) (hf : ∀ r ∈ s, r ≠ ⊤) : (sInf s).toReal = sInf (ENNReal.toReal '' s)

@[simp]

theorem ENNReal.ofReal_iInf {ι : Sort u_1} [Nonempty ι] (f : ι → ℝ) : ENNReal.ofReal (⨅ (i : ι), f i) = ⨅ (i : ι), ENNReal.ofReal (f i)

theorem ENNReal.iInf_add {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} : iInf f + a = ⨅ (i : ι), f i + a

theorem ENNReal.sub_iInf {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} : a - ⨅ (i : ι), f i = ⨆ (i : ι), a - f i

theorem ENNReal.sInf_add {a : ENNReal} {s : Set ENNReal} : sInf s + a = ⨅ b ∈ s, b + a

theorem ENNReal.add_iInf {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} : a + iInf f = ⨅ (b : ι), a + f b

theorem ENNReal.iInf_add_iInf {ι : Sort u_1} {f g : ι → ENNReal} (h : ∀ (i j : ι), ∃ (k : ι), f k + g k ≤ f i + g j) : iInf f + iInf g = ⨅ (a : ι), f a + g a

theorem ENNReal.iInf_add_iInf_of_monotone {ι : Type u_2} [Preorder ι] [IsCodirectedOrder ι] {f g : ι → ENNReal} (hf : Monotone f) (hg : Monotone g) : iInf f + iInf g = ⨅ (a : ι), f a + g a

theorem ENNReal.add_iInf₂ {ι : Sort u_1} {a : ENNReal} {κ : ι → Sort u_2} (f : (i : ι) → κ i → ENNReal) : a + ⨅ (i : ι), ⨅ (j : κ i), f i j = ⨅ (i : ι), ⨅ (j : κ i), a + f i j

theorem ENNReal.iInf₂_add {ι : Sort u_1} {a : ENNReal} {κ : ι → Sort u_2} (f : (i : ι) → κ i → ENNReal) : (⨅ (i : ι), ⨅ (j : κ i), f i j) + a = ⨅ (i : ι), ⨅ (j : κ i), f i j + a

theorem ENNReal.add_sInf {a : ENNReal} {s : Set ENNReal} : a + sInf s = ⨅ b ∈ s, a + b

theorem ENNReal.le_iInf_add_iInf {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} {κ : Sort u_2} {g : κ → ENNReal} (h : ∀ (i : ι) (j : κ), a ≤ f i + g j) : a ≤ iInf f + iInf g

theorem ENNReal.le_iInf₂_add_iInf₂ {ι : Sort u_1} {a : ENNReal} {κ : Sort u_2} {q₁ : ι → Sort u_3} {q₂ : κ → Sort u_4} {f : (i : ι) → q₁ i → ENNReal} {g : (k : κ) → q₂ k → ENNReal} (h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk) : a ≤ (⨅ (i : ι), ⨅ (qi : q₁ i), f i qi) + ⨅ (k : κ), ⨅ (qk : q₂ k), g k qk

@[simp]

theorem ENNReal.iInf_gt_eq_self (a : ENNReal) : ⨅ (b : ENNReal), ⨅ (_ : a < b), b = a

theorem ENNReal.exists_add_lt_of_add_lt {x y z : ENNReal} (h : y + z < x) : ∃ y' > y, ∃ z' > z, y' + z' < x

theorem ENNReal.toNNReal_iSup {ι : Sort u_1} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) : (iSup f).toNNReal = ⨆ (i : ι), (f i).toNNReal

theorem ENNReal.toNNReal_sSup (s : Set ENNReal) (hs : ∀ r ∈ s, r ≠ ⊤) : (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s)

theorem ENNReal.toReal_iSup {ι : Sort u_1} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) : (iSup f).toReal = ⨆ (i : ι), (f i).toReal

theorem ENNReal.toReal_sSup (s : Set ENNReal) (hf : ∀ r ∈ s, r ≠ ⊤) : (sSup s).toReal = sSup (ENNReal.toReal '' s)

theorem ENNReal.iSup_sub {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} : (⨆ (i : ι), f i) - a = ⨆ (i : ι), f i - a

@[simp]

theorem ENNReal.iSup_eq_zero {ι : Sort u_1} {f : ι → ENNReal} : ⨆ (i : ι), f i = 0 ↔ ∀ (i : ι), f i = 0

@[simp]

theorem ENNReal.iSup_zero {ι : Sort u_1} : ⨆ (x : ι), 0 = 0

theorem ENNReal.iSup_natCast : ⨆ (n : ℕ), ↑n = ⊤

theorem ENNReal.add_iSup {ι : Sort u_1} {a : ENNReal} [Nonempty ι] (f : ι → ENNReal) : a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i

theorem ENNReal.iSup_add {ι : Sort u_1} {a : ENNReal} [Nonempty ι] (f : ι → ENNReal) : (⨆ (i : ι), f i) + a = ⨆ (i : ι), f i + a

theorem ENNReal.add_biSup' {ι : Sort u_1} {a : ENNReal} {p : ι → Prop} (h : ∃ (i : ι), p i) (f : ι → ENNReal) : a + ⨆ (i : ι), ⨆ (_ : p i), f i = ⨆ (i : ι), ⨆ (_ : p i), a + f i

theorem ENNReal.biSup_add' {ι : Sort u_1} {a : ENNReal} {p : ι → Prop} (h : ∃ (i : ι), p i) (f : ι → ENNReal) : (⨆ (i : ι), ⨆ (_ : p i), f i) + a = ⨆ (i : ι), ⨆ (_ : p i), f i + a

theorem ENNReal.add_biSup {a : ENNReal} {ι : Type u_3} {s : Set ι} (hs : s.Nonempty) (f : ι → ENNReal) : a + ⨆ i ∈ s, f i = ⨆ i ∈ s, a + f i

theorem ENNReal.biSup_add {a : ENNReal} {ι : Type u_3} {s : Set ι} (hs : s.Nonempty) (f : ι → ENNReal) : (⨆ i ∈ s, f i) + a = ⨆ i ∈ s, f i + a

theorem ENNReal.add_sSup {s : Set ENNReal} {a : ENNReal} (hs : s.Nonempty) : a + sSup s = ⨆ b ∈ s, a + b

theorem ENNReal.sSup_add {s : Set ENNReal} {a : ENNReal} (hs : s.Nonempty) : sSup s + a = ⨆ b ∈ s, b + a

theorem ENNReal.iSup_add_iSup_le {ι : Sort u_1} {κ : Sort u_2} {f : ι → ENNReal} {a : ENNReal} [Nonempty ι] [Nonempty κ] {g : κ → ENNReal} (h : ∀ (i : ι) (j : κ), f i + g j ≤ a) : iSup f + iSup g ≤ a

theorem ENNReal.biSup_add_biSup_le' {ι : Sort u_1} {κ : Sort u_2} {f : ι → ENNReal} {a : ENNReal} {p : ι → Prop} {q : κ → Prop} (hp : ∃ (i : ι), p i) (hq : ∃ (j : κ), q j) {g : κ → ENNReal} (h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a) : (⨆ (i : ι), ⨆ (_ : p i), f i) + ⨆ (j : κ), ⨆ (_ : q j), g j ≤ a

theorem ENNReal.biSup_add_biSup_le {ι : Type u_3} {κ : Type u_4} {s : Set ι} {t : Set κ} (hs : s.Nonempty) (ht : t.Nonempty) {f : ι → ENNReal} {g : κ → ENNReal} {a : ENNReal} (h : ∀ i ∈ s, ∀ j ∈ t, f i + g j ≤ a) : (⨆ i ∈ s, f i) + ⨆ j ∈ t, g j ≤ a

theorem ENNReal.iSup_add_iSup {ι : Sort u_1} {f g : ι → ENNReal} (h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k) : iSup f + iSup g = ⨆ (i : ι), f i + g i

theorem ENNReal.iSup_add_iSup_of_monotone {ι : Type u_3} [Preorder ι] [IsDirectedOrder ι] {f g : ι → ENNReal} (hf : Monotone f) (hg : Monotone g) : iSup f + iSup g = ⨆ (a : ι), f a + g a

theorem ENNReal.sub_iSup {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} [Nonempty ι] (ha : a ≠ ⊤) : a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i

@[simp]

theorem ENNReal.iSup_lt_eq_self (a : ENNReal) : ⨆ (b : ENNReal), ⨆ (_ : b < a), b = a

theorem ENNReal.exists_lt_add_of_lt_add {x y z : ENNReal} (h : x < y + z) (hy : y ≠ 0) (hz : z ≠ 0) : ∃ y' < y, ∃ z' < z, x < y' + z'