Documentation

Mathlib.Data.ENNReal.Inv

Results about division in extended non-negative reals #

This file establishes basic properties related to the inversion and division operations on ℝ≥0∞. For instance, as a consequence of being a DivInvOneMonoid, ℝ≥0∞ inherits a power operation with integer exponent.

Main results #

A few order isomorphisms are worthy of mention:

theorem ENNReal.div_eq_inv_mul {a b : ENNReal} :
a / b = b⁻¹ * a
@[simp]
@[simp]
theorem ENNReal.coe_inv_le {r : NNReal} :
r⁻¹ (↑r)⁻¹
@[simp]
theorem ENNReal.coe_inv {r : NNReal} (hr : r 0) :
r⁻¹ = (↑r)⁻¹
@[simp]
theorem ENNReal.coe_div {r p : NNReal} (hr : r 0) :
↑(p / r) = p / r
theorem ENNReal.coe_div_le {r p : NNReal} :
↑(p / r) p / r
theorem ENNReal.div_zero {a : ENNReal} (h : a 0) :
a / 0 =
theorem ENNReal.inv_pow {a : ENNReal} {n : } :
(a ^ n)⁻¹ = a⁻¹ ^ n
theorem ENNReal.mul_inv_cancel {a : ENNReal} (h0 : a 0) (ht : a ) :
a * a⁻¹ = 1
theorem ENNReal.inv_mul_cancel {a : ENNReal} (h0 : a 0) (ht : a ) :
a⁻¹ * a = 1
theorem ENNReal.inv_mul_cancel_left' {a b : ENNReal} (ha₀ : a = 0b = 0) (ha : a = b = 0) :
a⁻¹ * (a * b) = b

See ENNReal.inv_mul_cancel_left for a simpler version assuming a ≠ 0, a ≠ ∞.

theorem ENNReal.inv_mul_cancel_left {a b : ENNReal} (ha₀ : a 0) (ha : a ) :
a⁻¹ * (a * b) = b

See ENNReal.inv_mul_cancel_left' for a stronger version.

theorem ENNReal.mul_inv_cancel_left' {a b : ENNReal} (ha₀ : a = 0b = 0) (ha : a = b = 0) :
a * (a⁻¹ * b) = b

See ENNReal.mul_inv_cancel_left for a simpler version assuming a ≠ 0, a ≠ ∞.

theorem ENNReal.mul_inv_cancel_left {a b : ENNReal} (ha₀ : a 0) (ha : a ) :
a * (a⁻¹ * b) = b

See ENNReal.mul_inv_cancel_left' for a stronger version.

theorem ENNReal.mul_inv_cancel_right' {a b : ENNReal} (hb₀ : b = 0a = 0) (hb : b = a = 0) :
a * b * b⁻¹ = a

See ENNReal.mul_inv_cancel_right for a simpler version assuming b ≠ 0, b ≠ ∞.

theorem ENNReal.mul_inv_cancel_right {a b : ENNReal} (hb₀ : b 0) (hb : b ) :
a * b * b⁻¹ = a

See ENNReal.mul_inv_cancel_right' for a stronger version.

theorem ENNReal.inv_mul_cancel_right' {a b : ENNReal} (hb₀ : b = 0a = 0) (hb : b = a = 0) :
a * b⁻¹ * b = a

See ENNReal.inv_mul_cancel_right for a simpler version assuming b ≠ 0, b ≠ ∞.

theorem ENNReal.inv_mul_cancel_right {a b : ENNReal} (hb₀ : b 0) (hb : b ) :
a * b⁻¹ * b = a

See ENNReal.inv_mul_cancel_right' for a stronger version.

theorem ENNReal.mul_div_cancel_right' {a b : ENNReal} (hb₀ : b = 0a = 0) (hb : b = a = 0) :
a * b / b = a

See ENNReal.mul_div_cancel_right for a simpler version assuming b ≠ 0, b ≠ ∞.

theorem ENNReal.mul_div_cancel_right {a b : ENNReal} (hb₀ : b 0) (hb : b ) :
a * b / b = a

See ENNReal.mul_div_cancel_right' for a stronger version.

theorem ENNReal.div_mul_cancel' {a b : ENNReal} (ha₀ : a = 0b = 0) (ha : a = b = 0) :
b / a * a = b

See ENNReal.div_mul_cancel for a simpler version assuming a ≠ 0, a ≠ ∞.

theorem ENNReal.div_mul_cancel {a b : ENNReal} (ha₀ : a 0) (ha : a ) :
b / a * a = b

See ENNReal.div_mul_cancel' for a stronger version.

theorem ENNReal.mul_div_cancel' {a b : ENNReal} (ha₀ : a = 0b = 0) (ha : a = b = 0) :
a * (b / a) = b

See ENNReal.mul_div_cancel for a simpler version assuming a ≠ 0, a ≠ ∞.

theorem ENNReal.mul_div_cancel {a b : ENNReal} (ha₀ : a 0) (ha : a ) :
a * (b / a) = b

See ENNReal.mul_div_cancel' for a stronger version.

theorem ENNReal.mul_comm_div {a b c : ENNReal} :
a / b * c = a * (c / b)
theorem ENNReal.mul_div_right_comm {a b c : ENNReal} :
a * b / c = a / c * b
@[simp]
theorem ENNReal.inv_eq_one {a : ENNReal} :
a⁻¹ = 1 a = 1
@[simp]
theorem ENNReal.inv_eq_top {a : ENNReal} :
a⁻¹ = a = 0

Alias of the reverse direction of ENNReal.inv_ne_top.

@[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 <
theorem ENNReal.div_ne_top {x y : ENNReal} (h1 : x ) (h2 : y 0) :
x / y
@[simp]
theorem ENNReal.inv_eq_zero {a : ENNReal} :
a⁻¹ = 0 a =
theorem ENNReal.div_pos {a b : ENNReal} (ha : a 0) (hb : b ) :
0 < a / b
theorem ENNReal.inv_mul_le_iff {x y z : ENNReal} (h1 : x 0) (h2 : x ) :
x⁻¹ * y z y x * z
theorem ENNReal.mul_inv_le_iff {x y z : ENNReal} (h1 : y 0) (h2 : y ) :
x * y⁻¹ z x z * y
theorem ENNReal.div_le_iff {x y z : ENNReal} (h1 : y 0) (h2 : y ) :
x / y z x z * y
theorem ENNReal.div_le_iff' {x y z : ENNReal} (h1 : y 0) (h2 : y ) :
x / y z x y * z
theorem ENNReal.mul_inv {a b : ENNReal} (ha : a 0 b ) (hb : a b 0) :
(a * b)⁻¹ = a⁻¹ * b⁻¹
theorem ENNReal.inv_div {a b : ENNReal} (htop : b a ) (hzero : b 0 a 0) :
(a / b)⁻¹ = b / a
theorem ENNReal.mul_div_mul_left {c : ENNReal} (a b : ENNReal) (hc : c 0) (hc' : c ) :
c * a / (c * b) = a / b
theorem ENNReal.mul_div_mul_right {c : ENNReal} (a b : ENNReal) (hc : c 0) (hc' : c ) :
a * c / (b * c) = a / b
theorem ENNReal.sub_div {a b c : ENNReal} (h : 0 < bb < ac 0) :
(a - b) / c = a / c - b / c
@[simp]
theorem ENNReal.inv_pos {a : ENNReal} :
@[simp]
theorem ENNReal.inv_lt_inv {a b : ENNReal} :
a⁻¹ < b⁻¹ b < a
@[simp]
theorem ENNReal.inv_le_inv' {a b : ENNReal} (h : a b) :
theorem ENNReal.inv_lt_inv' {a b : ENNReal} (h : a < b) :
@[simp]
theorem ENNReal.inv_le_one {a : ENNReal} :
a⁻¹ 1 1 a
@[simp]
theorem ENNReal.inv_lt_one {a : ENNReal} :
a⁻¹ < 1 1 < a
@[simp]
theorem ENNReal.one_lt_inv {a : ENNReal} :
1 < a⁻¹ a < 1

The inverse map fun x ↦ x⁻¹ is an order isomorphism between ℝ≥0∞ and its OrderDual

Equations
    Instances For
      @[simp]
      theorem ENNReal.div_top {a : ENNReal} :
      a / = 0
      @[simp]
      theorem ENNReal.top_div_coe {p : NNReal} :
      / p =
      @[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
      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
      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
      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
      @[simp]
      theorem ENNReal.div_self_le_one {a : ENNReal} :
      a / a 1
      @[simp]
      @[simp]
      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
      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.div_lt_of_lt_mul {a b c : ENNReal} (h : a < b * c) :
      a / c < b
      theorem ENNReal.div_lt_of_lt_mul' {a b c : ENNReal} (h : a < b * c) :
      a / b < c
      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
      theorem ENNReal.div_le_div {a b c d : ENNReal} (hab : a b) (hdc : d c) :
      a / c b / d
      theorem ENNReal.div_le_div_left {a b : ENNReal} (h : a b) (c : ENNReal) :
      c / b c / a
      theorem ENNReal.div_le_div_right {a b : ENNReal} (h : a b) (c : ENNReal) :
      a / c b / c
      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
      theorem ENNReal.le_of_forall_nnreal_lt {x y : ENNReal} (h : ∀ (r : NNReal), r < xr y) :
      x y
      theorem ENNReal.eq_of_forall_nnreal_iff {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 < rr < xr y) :
      x y
      theorem ENNReal.eq_top_of_forall_nnreal_le {x : ENNReal} (h : ∀ (r : NNReal), r x) :
      x =
      theorem ENNReal.add_div {a b c : ENNReal} :
      (a + b) / c = a / c + b / c
      theorem ENNReal.div_add_div_same {a b c : ENNReal} :
      a / c + b / c = (a + b) / c
      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
      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
      @[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_eq_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
      theorem ENNReal.div_ne_zero {a b : ENNReal} :
      a / b 0 a 0 b
      theorem ENNReal.div_mul {b c : ENNReal} (a : ENNReal) (h0 : b 0 c 0) (htop : b c ) :
      a / b * c = a / (b / c)
      theorem ENNReal.mul_div_mul_comm {a b c d : ENNReal} (hc : c 0 d ) (hd : c d 0) :
      a * b / (c * d) = a / c * (b / d)
      theorem ENNReal.half_pos {a : ENNReal} (h : a 0) :
      0 < a / 2
      theorem ENNReal.half_lt_self {a : ENNReal} (hz : a 0) (ht : a ) :
      a / 2 < a
      theorem ENNReal.sub_half {a : ENNReal} (h : a ) :
      a - a / 2 = a / 2
      theorem ENNReal.mul_le_of_forall_lt {a b c : ENNReal} (h : a' < a, b' < b, a' * b' c) :
      a * b c
      theorem ENNReal.le_mul_of_forall_lt {a b c : ENNReal} (h₁ : a 0 b ) (h₂ : a b 0) (h : a' > a, b' > b, c a' * b') :
      c a * b

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

      Equations
        Instances For
          def ENNReal.orderIsoIicCoe (a : NNReal) :
          (Set.Iic a) ≃o (Set.Iic a)

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

          Equations
            Instances For
              @[simp]
              theorem ENNReal.orderIsoIicCoe_apply_coe (a : NNReal) (a✝ : (Set.Iic a)) :
              ((orderIsoIicCoe a) a✝) = (↑a✝).toNNReal
              @[simp]
              theorem ENNReal.orderIsoIicCoe_symm_apply_coe (a : NNReal) (b : (Set.Iic a)) :
              ((orderIsoIicCoe a).symm b) = b

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

              Equations
                Instances For
                  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 > 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 > 0, (↑n)⁻¹ * a < b
                  theorem ENNReal.exists_nnreal_pos_mul_lt {a b : ENNReal} (ha : a ) (hb : b 0) :
                  n > 0, n * a < b
                  theorem ENNReal.exists_inv_two_pow_lt {a : ENNReal} (ha : a 0) :
                  ∃ (n : ), 2⁻¹ ^ n < a
                  @[simp]
                  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.zpow_ne_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_iUnion_Ico_zpow {y : ENNReal} (hy : 1 < y) (h'y : y ) :
                  Set.Ioo 0 = ⋃ (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) :
                  Monotone fun (x_1 : ) => x ^ x_1
                  theorem ENNReal.zpow_add {x : ENNReal} (hx : x 0) (h'x : x ) (m n : ) :
                  x ^ (m + n) = x ^ m * x ^ n
                  theorem ENNReal.zpow_neg {x : ENNReal} (x_ne_zero : x 0) (x_ne_top : x ) (m : ) :
                  x ^ (-m) = (x ^ m)⁻¹
                  theorem ENNReal.zpow_sub {x : ENNReal} (x_ne_zero : x 0) (x_ne_top : x ) (m n : ) :
                  x ^ (m - n) = x ^ m * (x ^ n)⁻¹
                  @[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
                  @[deprecated ENNReal.iSup_zero (since := "2024-10-22")]
                  theorem ENNReal.iSup_zero_eq_zero {ι : Sort u_1} :
                  ⨆ (x : ι), 0 = 0

                  Alias of ENNReal.iSup_zero.

                  theorem ENNReal.iSup_natCast :
                  ⨆ (n : ), n =
                  @[simp]
                  theorem ENNReal.iSup_lt_eq_self (a : ENNReal) :
                  ⨆ (b : ENNReal), ⨆ (_ : b < a), b = a

                  Left multiplication by a nonzero finite a as an order isomorphism.

                  Equations
                    Instances For
                      @[simp]
                      @[simp]
                      theorem ENNReal.mulLeftOrderIso_apply (a : ENNReal) (ha : IsUnit a) (x : ENNReal) :
                      (a.mulLeftOrderIso ha) x = a * x

                      Right multiplication by a nonzero finite a as an order isomorphism.

                      Equations
                        Instances For
                          @[simp]
                          theorem ENNReal.mulRightOrderIso_apply (a : ENNReal) (ha : IsUnit a) (x : ENNReal) :
                          (a.mulRightOrderIso ha) x = x * a
                          theorem ENNReal.mul_iSup {ι : Sort u_1} (a : ENNReal) (f : ιENNReal) :
                          a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
                          theorem ENNReal.iSup_mul {ι : Sort u_1} (f : ιENNReal) (a : ENNReal) :
                          (⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a
                          theorem ENNReal.mul_sSup {s : Set ENNReal} {a : ENNReal} :
                          a * sSup s = bs, a * b
                          theorem ENNReal.sSup_mul {s : Set ENNReal} {a : ENNReal} :
                          sSup s * a = bs, b * a
                          theorem ENNReal.iSup_div {ι : Sort u_1} (f : ιENNReal) (a : ENNReal) :
                          iSup f / a = ⨆ (i : ι), f i / a
                          theorem ENNReal.sSup_div (s : Set ENNReal) (a : ENNReal) :
                          sSup s / a = bs, b / a
                          theorem ENNReal.mul_iInf' {ι : Sort u_1} {f : ιENNReal} {a : ENNReal} (hinfty : a = ⨅ (i : ι), f i = 0∃ (i : ι), f i = 0) (h₀ : a = 0Nonempty ι) :
                          a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i

                          Very general version for distributivity of multiplication over an infimum.

                          See ENNReal.mul_iInf_of_ne for the special case assuming a ≠ 0 and a ≠ ∞, and ENNReal.mul_iInf for the special case assuming Nonempty ι.

                          theorem ENNReal.iInf_mul' {ι : Sort u_1} {f : ιENNReal} {a : ENNReal} (hinfty : a = ⨅ (i : ι), f i = 0∃ (i : ι), f i = 0) (h₀ : a = 0Nonempty ι) :
                          (⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a

                          Very general version for distributivity of multiplication over an infimum.

                          See ENNReal.iInf_mul_of_ne for the special case assuming a ≠ 0 and a ≠ ∞, and ENNReal.iInf_mul for the special case assuming Nonempty ι.

                          theorem ENNReal.mul_iInf_of_ne {ι : Sort u_1} {f : ιENNReal} {a : ENNReal} (ha₀ : a 0) (ha : a ) :
                          a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i

                          If a ≠ 0 and a ≠ ∞, then right multiplication by a maps infimum to infimum.

                          See ENNReal.mul_iInf' for the general case, and ENNReal.iInf_mul for another special case that assumes Nonempty ι but does not require a ≠ 0, and ENNReal.

                          theorem ENNReal.iInf_mul_of_ne {ι : Sort u_1} {f : ιENNReal} {a : ENNReal} (ha₀ : a 0) (ha : a ) :
                          (⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a

                          If a ≠ 0 and a ≠ ∞, then right multiplication by a maps infimum to infimum.

                          See ENNReal.iInf_mul' for the general case, and ENNReal.iInf_mul for another special case that assumes Nonempty ι but does not require a ≠ 0.

                          theorem ENNReal.mul_iInf {ι : Sort u_1} {f : ιENNReal} {a : ENNReal} [Nonempty ι] (hinfty : a = ⨅ (i : ι), f i = 0∃ (i : ι), f i = 0) :
                          a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i

                          See ENNReal.mul_iInf' for the general case, and ENNReal.mul_iInf_of_ne for another special case that assumes a ≠ 0 but does not require Nonempty ι.

                          theorem ENNReal.iInf_mul {ι : Sort u_1} {f : ιENNReal} {a : ENNReal} [Nonempty ι] (hinfty : a = ⨅ (i : ι), f i = 0∃ (i : ι), f i = 0) :
                          (⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a

                          See ENNReal.iInf_mul' for the general case, and ENNReal.iInf_mul_of_ne for another special case that assumes a ≠ 0 but does not require Nonempty ι.

                          theorem ENNReal.iInf_div' {ι : Sort u_1} {f : ιENNReal} {a : ENNReal} (hinfty : a = 0⨅ (i : ι), f i = 0∃ (i : ι), f i = 0) (h₀ : a = Nonempty ι) :
                          (⨅ (i : ι), f i) / a = ⨅ (i : ι), f i / a

                          Very general version for distributivity of division over an infimum.

                          See ENNReal.iInf_div_of_ne for the special case assuming a ≠ 0 and a ≠ ∞, and ENNReal.iInf_div for the special case assuming Nonempty ι.

                          theorem ENNReal.iInf_div_of_ne {ι : Sort u_1} {f : ιENNReal} {a : ENNReal} (ha₀ : a 0) (ha : a ) :
                          (⨅ (i : ι), f i) / a = ⨅ (i : ι), f i / a

                          If a ≠ 0 and a ≠ ∞, then division by a maps infimum to infimum.

                          See ENNReal.iInf_div' for the general case, and ENNReal.iInf_div for another special case that assumes Nonempty ι but does not require a ≠ ∞.

                          theorem ENNReal.iInf_div {ι : Sort u_1} {f : ιENNReal} {a : ENNReal} [Nonempty ι] (hinfty : a = 0⨅ (i : ι), f i = 0∃ (i : ι), f i = 0) :
                          (⨅ (i : ι), f i) / a = ⨅ (i : ι), f i / a

                          See ENNReal.iInf_div' for the general case, and ENNReal.iInf_div_of_ne for another special case that assumes a ≠ ∞ but does not require Nonempty ι.

                          theorem ENNReal.inv_iInf {ι : Sort u_1} (f : ιENNReal) :
                          (⨅ (i : ι), f i)⁻¹ = ⨆ (i : ι), (f i)⁻¹
                          theorem ENNReal.inv_iSup {ι : Sort u_1} (f : ιENNReal) :
                          (⨆ (i : ι), f i)⁻¹ = ⨅ (i : ι), (f i)⁻¹
                          theorem ENNReal.inv_sInf (s : Set ENNReal) :
                          (sInf s)⁻¹ = as, a⁻¹
                          theorem ENNReal.inv_sSup (s : Set ENNReal) :
                          (sSup s)⁻¹ = as, a⁻¹
                          theorem ENNReal.le_iInf_mul {ι : Type u_3} (u v : ιENNReal) :
                          (⨅ (i : ι), u i) * ⨅ (i : ι), v i ⨅ (i : ι), u i * v i
                          theorem ENNReal.iSup_mul_le {ι : Type u_3} {u v : ιENNReal} :
                          ⨆ (i : ι), u i * v i (⨆ (i : ι), u i) * ⨆ (i : ι), v i
                          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 + is, f i = is, a + f i
                          theorem ENNReal.biSup_add {a : ENNReal} {ι : Type u_3} {s : Set ι} (hs : s.Nonempty) (f : ιENNReal) :
                          (⨆ is, f i) + a = is, f i + a
                          theorem ENNReal.add_sSup {s : Set ENNReal} {a : ENNReal} (hs : s.Nonempty) :
                          a + sSup s = bs, a + b
                          theorem ENNReal.sSup_add {s : Set ENNReal} {a : ENNReal} (hs : s.Nonempty) :
                          sSup s + a = bs, 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 jf 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 : is, jt, f i + g j a) :
                          (⨆ is, f i) + jt, 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 ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] {f g : ιENNReal} (hf : Monotone f) (hg : Monotone g) :
                          iSup f + iSup g = ⨆ (a : ι), f a + g a
                          theorem ENNReal.le_iInf_mul_iInf {ι : Sort u_1} {κ : Sort u_2} {f : ιENNReal} {a : ENNReal} {g : κENNReal} (hf : ∃ (i : ι), f i ) (hg : ∃ (j : κ), g j ) (ha : ∀ (i : ι) (j : κ), a f i * g j) :
                          a (⨅ (i : ι), f i) * ⨅ (j : κ), g j
                          theorem ENNReal.iInf_mul_iInf {ι : Sort u_1} {f g : ιENNReal} (hf : ∃ (i : ι), f i ) (hg : ∃ (j : ι), g j ) (h : ∀ (i j : ι), ∃ (k : ι), f k * g k f i * g j) :
                          (⨅ (i : ι), f i) * ⨅ (i : ι), g i = ⨅ (i : ι), f i * g i
                          theorem ENNReal.smul_iSup {ι : Sort u_1} {R : Type u_3} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (f : ιENNReal) (c : R) :
                          c ⨆ (i : ι), f i = ⨆ (i : ι), c f i
                          theorem ENNReal.smul_sSup {R : Type u_3} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (s : Set ENNReal) (c : R) :
                          c sSup s = as, c a
                          theorem ENNReal.sub_iSup {ι : Sort u_1} {f : ιENNReal} {a : ENNReal} [Nonempty ι] (ha : a ) :
                          a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
                          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'
                          @[simp]
                          @[simp]
                          theorem ENNReal.toReal_div (a b : ENNReal) :
                          (a / b).toReal = a.toReal / b.toReal