# Power function on ℝ≥0 and ℝ≥0∞#

We construct the power functions x ^ y where

• x is a nonnegative real number and y is a real number;
• x is a number from [0, +∞] (a.k.a. ℝ≥0∞) and y is a real number.

We also prove basic properties of these functions.

noncomputable def NNReal.rpow (x : NNReal) (y : ) :

The nonnegative real power function x^y, defined for x : ℝ≥0 and y : ℝ as the restriction of the real power function. For x > 0, it is equal to exp (y log x). For x = 0, one sets 0 ^ 0 = 1 and 0 ^ y = 0 for y ≠ 0.

Equations
• = { val := x ^ y, property := }
Instances For
noncomputable instance NNReal.instPowNNRealReal :
Equations
@[simp]
theorem NNReal.rpow_eq_pow (x : NNReal) (y : ) :
= x ^ y
@[simp]
theorem NNReal.coe_rpow (x : NNReal) (y : ) :
(x ^ y) = x ^ y
@[simp]
theorem NNReal.rpow_zero (x : NNReal) :
x ^ 0 = 1
@[simp]
theorem NNReal.rpow_eq_zero_iff {x : NNReal} {y : } :
x ^ y = 0 x = 0 y 0
@[simp]
theorem NNReal.zero_rpow {x : } (h : x 0) :
0 ^ x = 0
@[simp]
theorem NNReal.rpow_one (x : NNReal) :
x ^ 1 = x
@[simp]
theorem NNReal.one_rpow (x : ) :
1 ^ x = 1
theorem NNReal.rpow_add {x : NNReal} (hx : x 0) (y : ) (z : ) :
x ^ (y + z) = x ^ y * x ^ z
theorem NNReal.rpow_add' (x : NNReal) {y : } {z : } (h : y + z 0) :
x ^ (y + z) = x ^ y * x ^ z
theorem NNReal.rpow_of_add_eq {w : } {y : } {z : } (x : NNReal) (hw : w 0) (h : y + z = w) :
x ^ w = x ^ y * x ^ z

Variant of NNReal.rpow_add' that avoids having to prove y + z = w twice.

theorem NNReal.rpow_mul (x : NNReal) (y : ) (z : ) :
x ^ (y * z) = (x ^ y) ^ z
theorem NNReal.rpow_neg (x : NNReal) (y : ) :
x ^ (-y) = (x ^ y)⁻¹
theorem NNReal.rpow_neg_one (x : NNReal) :
x ^ (-1) = x⁻¹
theorem NNReal.rpow_sub {x : NNReal} (hx : x 0) (y : ) (z : ) :
x ^ (y - z) = x ^ y / x ^ z
theorem NNReal.rpow_sub' (x : NNReal) {y : } {z : } (h : y - z 0) :
x ^ (y - z) = x ^ y / x ^ z
theorem NNReal.rpow_inv_rpow_self {y : } (hy : y 0) (x : NNReal) :
(x ^ y) ^ (1 / y) = x
theorem NNReal.rpow_self_rpow_inv {y : } (hy : y 0) (x : NNReal) :
(x ^ (1 / y)) ^ y = x
theorem NNReal.inv_rpow (x : NNReal) (y : ) :
x⁻¹ ^ y = (x ^ y)⁻¹
theorem NNReal.div_rpow (x : NNReal) (y : NNReal) (z : ) :
(x / y) ^ z = x ^ z / y ^ z
theorem NNReal.sqrt_eq_rpow (x : NNReal) :
NNReal.sqrt x = x ^ (1 / 2)
@[simp]
theorem NNReal.rpow_nat_cast (x : NNReal) (n : ) :
x ^ n = x ^ n
@[simp]
theorem NNReal.rpow_ofNat (x : NNReal) (n : ) [] :
x ^ = x ^
theorem NNReal.rpow_two (x : NNReal) :
x ^ 2 = x ^ 2
theorem NNReal.mul_rpow {x : NNReal} {y : NNReal} {z : } :
(x * y) ^ z = x ^ z * y ^ z
@[simp]
theorem NNReal.rpowMonoidHom_apply (r : ) :
∀ (x : NNReal), x = x ^ r

rpow as a MonoidHom

Equations
• = { toOneHom := { toFun := fun (x : NNReal) => x ^ r, map_one' := }, map_mul' := }
Instances For
theorem NNReal.list_prod_map_rpow (l : ) (r : ) :
List.prod (List.map (fun (x : NNReal) => x ^ r) l) = ^ r

rpow variant of List.prod_map_pow for ℝ≥0

theorem NNReal.list_prod_map_rpow' {ι : Type u_1} (l : List ι) (f : ιNNReal) (r : ) :
List.prod (List.map (fun (x : ι) => f x ^ r) l) = List.prod (List.map f l) ^ r
theorem NNReal.multiset_prod_map_rpow {ι : Type u_1} (s : ) (f : ιNNReal) (r : ) :
Multiset.prod (Multiset.map (fun (x : ι) => f x ^ r) s) = ^ r

rpow version of Multiset.prod_map_pow for ℝ≥0.

theorem NNReal.finset_prod_rpow {ι : Type u_1} (s : ) (f : ιNNReal) (r : ) :
(Finset.prod s fun (i : ι) => f i ^ r) = (Finset.prod s fun (i : ι) => f i) ^ r

rpow version of Finset.prod_pow for ℝ≥0.

theorem Real.list_prod_map_rpow (l : ) (hl : xl, 0 x) (r : ) :
List.prod (List.map (fun (x : ) => x ^ r) l) = ^ r

rpow version of List.prod_map_pow for Real.

theorem Real.list_prod_map_rpow' {ι : Type u_1} (l : List ι) (f : ι) (hl : il, 0 f i) (r : ) :
List.prod (List.map (fun (x : ι) => f x ^ r) l) = List.prod (List.map f l) ^ r
theorem Real.multiset_prod_map_rpow {ι : Type u_1} (s : ) (f : ι) (hs : is, 0 f i) (r : ) :
Multiset.prod (Multiset.map (fun (x : ι) => f x ^ r) s) = ^ r

rpow version of Multiset.prod_map_pow.

theorem Real.finset_prod_rpow {ι : Type u_1} (s : ) (f : ι) (hs : is, 0 f i) (r : ) :
(Finset.prod s fun (i : ι) => f i ^ r) = (Finset.prod s fun (i : ι) => f i) ^ r

rpow version of Finset.prod_pow.

theorem NNReal.rpow_le_rpow {x : NNReal} {y : NNReal} {z : } (h₁ : x y) (h₂ : 0 z) :
x ^ z y ^ z
theorem NNReal.rpow_lt_rpow {x : NNReal} {y : NNReal} {z : } (h₁ : x < y) (h₂ : 0 < z) :
x ^ z < y ^ z
theorem NNReal.rpow_lt_rpow_iff {x : NNReal} {y : NNReal} {z : } (hz : 0 < z) :
x ^ z < y ^ z x < y
theorem NNReal.rpow_le_rpow_iff {x : NNReal} {y : NNReal} {z : } (hz : 0 < z) :
x ^ z y ^ z x y
theorem NNReal.le_rpow_one_div_iff {x : NNReal} {y : NNReal} {z : } (hz : 0 < z) :
x y ^ (1 / z) x ^ z y
theorem NNReal.rpow_one_div_le_iff {x : NNReal} {y : NNReal} {z : } (hz : 0 < z) :
x ^ (1 / z) y x y ^ z
theorem NNReal.rpow_lt_rpow_of_exponent_lt {x : NNReal} {y : } {z : } (hx : 1 < x) (hyz : y < z) :
x ^ y < x ^ z
theorem NNReal.rpow_le_rpow_of_exponent_le {x : NNReal} {y : } {z : } (hx : 1 x) (hyz : y z) :
x ^ y x ^ z
theorem NNReal.rpow_lt_rpow_of_exponent_gt {x : NNReal} {y : } {z : } (hx0 : 0 < x) (hx1 : x < 1) (hyz : z < y) :
x ^ y < x ^ z
theorem NNReal.rpow_le_rpow_of_exponent_ge {x : NNReal} {y : } {z : } (hx0 : 0 < x) (hx1 : x 1) (hyz : z y) :
x ^ y x ^ z
theorem NNReal.rpow_pos {p : } {x : NNReal} (hx_pos : 0 < x) :
0 < x ^ p
theorem NNReal.rpow_lt_one {x : NNReal} {z : } (hx1 : x < 1) (hz : 0 < z) :
x ^ z < 1
theorem NNReal.rpow_le_one {x : NNReal} {z : } (hx2 : x 1) (hz : 0 z) :
x ^ z 1
theorem NNReal.rpow_lt_one_of_one_lt_of_neg {x : NNReal} {z : } (hx : 1 < x) (hz : z < 0) :
x ^ z < 1
theorem NNReal.rpow_le_one_of_one_le_of_nonpos {x : NNReal} {z : } (hx : 1 x) (hz : z 0) :
x ^ z 1
theorem NNReal.one_lt_rpow {x : NNReal} {z : } (hx : 1 < x) (hz : 0 < z) :
1 < x ^ z
theorem NNReal.one_le_rpow {x : NNReal} {z : } (h : 1 x) (h₁ : 0 z) :
1 x ^ z
theorem NNReal.one_lt_rpow_of_pos_of_lt_one_of_neg {x : NNReal} {z : } (hx1 : 0 < x) (hx2 : x < 1) (hz : z < 0) :
1 < x ^ z
theorem NNReal.one_le_rpow_of_pos_of_le_one_of_nonpos {x : NNReal} {z : } (hx1 : 0 < x) (hx2 : x 1) (hz : z 0) :
1 x ^ z
theorem NNReal.rpow_le_self_of_le_one {x : NNReal} {z : } (hx : x 1) (h_one_le : 1 z) :
x ^ z x
theorem NNReal.rpow_left_injective {x : } (hx : x 0) :
Function.Injective fun (y : NNReal) => y ^ x
theorem NNReal.rpow_eq_rpow_iff {x : NNReal} {y : NNReal} {z : } (hz : z 0) :
x ^ z = y ^ z x = y
theorem NNReal.rpow_left_surjective {x : } (hx : x 0) :
Function.Surjective fun (y : NNReal) => y ^ x
theorem NNReal.rpow_left_bijective {x : } (hx : x 0) :
Function.Bijective fun (y : NNReal) => y ^ x
theorem NNReal.eq_rpow_one_div_iff {x : NNReal} {y : NNReal} {z : } (hz : z 0) :
x = y ^ (1 / z) x ^ z = y
theorem NNReal.rpow_one_div_eq_iff {x : NNReal} {y : NNReal} {z : } (hz : z 0) :
x ^ (1 / z) = y x = y ^ z
@[simp]
theorem NNReal.rpow_rpow_inv {y : } (hy : y 0) (x : NNReal) :
(x ^ y) ^ y⁻¹ = x
@[simp]
theorem NNReal.rpow_inv_rpow {y : } (hy : y 0) (x : NNReal) :
(x ^ y⁻¹) ^ y = x
theorem NNReal.pow_rpow_inv_natCast (x : NNReal) {n : } (hn : n 0) :
(x ^ n) ^ (n)⁻¹ = x
theorem NNReal.rpow_inv_natCast_pow (x : NNReal) {n : } (hn : n 0) :
(x ^ (n)⁻¹) ^ n = x
theorem Real.toNNReal_rpow_of_nonneg {x : } {y : } (hx : 0 x) :
theorem NNReal.strictMono_rpow_of_pos {z : } (h : 0 < z) :
StrictMono fun (x : NNReal) => x ^ z
theorem NNReal.monotone_rpow_of_nonneg {z : } (h : 0 z) :
Monotone fun (x : NNReal) => x ^ z
@[simp]
theorem NNReal.orderIsoRpow_apply (y : ) (hy : 0 < y) (x : NNReal) :
() x = x ^ y
def NNReal.orderIsoRpow (y : ) (hy : 0 < y) :

Bundles fun x : ℝ≥0 => x ^ y into an order isomorphism when y : ℝ is positive, where the inverse is fun x : ℝ≥0 => x ^ (1 / y).

Equations
Instances For
theorem NNReal.orderIsoRpow_symm_eq (y : ) (hy : 0 < y) :
noncomputable def ENNReal.rpow :
ENNReal

The real power function x^y on extended nonnegative reals, defined for x : ℝ≥0∞ and y : ℝ as the restriction of the real power function if 0 < x < ⊤, and with the natural values for 0 and ⊤ (i.e., 0 ^ x = 0 for x > 0, 1 for x = 0 and ⊤ for x < 0, and ⊤ ^ x = 1 / 0 ^ x).

Equations
• ENNReal.rpow x✝ x = match x✝, x with | some x, y => if x = 0 y < 0 then else (x ^ y) | none, y => if 0 < y then else if y = 0 then 1 else 0
Instances For
@[simp]
theorem ENNReal.rpow_eq_pow (x : ENNReal) (y : ) :
= x ^ y
@[simp]
theorem ENNReal.rpow_zero {x : ENNReal} :
x ^ 0 = 1
theorem ENNReal.top_rpow_def (y : ) :
^ y = if 0 < y then else if y = 0 then 1 else 0
@[simp]
theorem ENNReal.top_rpow_of_pos {y : } (h : 0 < y) :
@[simp]
theorem ENNReal.top_rpow_of_neg {y : } (h : y < 0) :
^ y = 0
@[simp]
theorem ENNReal.zero_rpow_of_pos {y : } (h : 0 < y) :
0 ^ y = 0
@[simp]
theorem ENNReal.zero_rpow_of_neg {y : } (h : y < 0) :
0 ^ y =
theorem ENNReal.zero_rpow_def (y : ) :
0 ^ y = if 0 < y then 0 else if y = 0 then 1 else
@[simp]
theorem ENNReal.zero_rpow_mul_self (y : ) :
0 ^ y * 0 ^ y = 0 ^ y
theorem ENNReal.coe_rpow_of_ne_zero {x : NNReal} (h : x 0) (y : ) :
x ^ y = (x ^ y)
theorem ENNReal.coe_rpow_of_nonneg (x : NNReal) {y : } (h : 0 y) :
x ^ y = (x ^ y)
theorem ENNReal.coe_rpow_def (x : NNReal) (y : ) :
x ^ y = if x = 0 y < 0 then else (x ^ y)
@[simp]
theorem ENNReal.rpow_one (x : ENNReal) :
x ^ 1 = x
@[simp]
theorem ENNReal.one_rpow (x : ) :
1 ^ x = 1
@[simp]
theorem ENNReal.rpow_eq_zero_iff {x : ENNReal} {y : } :
x ^ y = 0 x = 0 0 < y x = y < 0
theorem ENNReal.rpow_eq_zero_iff_of_pos {x : ENNReal} {y : } (hy : 0 < y) :
x ^ y = 0 x = 0
@[simp]
theorem ENNReal.rpow_eq_top_iff {x : ENNReal} {y : } :
x ^ y = x = 0 y < 0 x = 0 < y
theorem ENNReal.rpow_eq_top_iff_of_pos {x : ENNReal} {y : } (hy : 0 < y) :
x ^ y = x =
theorem ENNReal.rpow_lt_top_iff_of_pos {x : ENNReal} {y : } (hy : 0 < y) :
x ^ y < x <
theorem ENNReal.rpow_eq_top_of_nonneg (x : ENNReal) {y : } (hy0 : 0 y) :
x ^ y = x =
theorem ENNReal.rpow_ne_top_of_nonneg {x : ENNReal} {y : } (hy0 : 0 y) (h : x ) :
x ^ y
theorem ENNReal.rpow_lt_top_of_nonneg {x : ENNReal} {y : } (hy0 : 0 y) (h : x ) :
x ^ y <
theorem ENNReal.rpow_add {x : ENNReal} (y : ) (z : ) (hx : x 0) (h'x : x ) :
x ^ (y + z) = x ^ y * x ^ z
theorem ENNReal.rpow_neg (x : ENNReal) (y : ) :
x ^ (-y) = (x ^ y)⁻¹
theorem ENNReal.rpow_sub {x : ENNReal} (y : ) (z : ) (hx : x 0) (h'x : x ) :
x ^ (y - z) = x ^ y / x ^ z
theorem ENNReal.rpow_neg_one (x : ENNReal) :
x ^ (-1) = x⁻¹
theorem ENNReal.rpow_mul (x : ENNReal) (y : ) (z : ) :
x ^ (y * z) = (x ^ y) ^ z
@[simp]
theorem ENNReal.rpow_nat_cast (x : ENNReal) (n : ) :
x ^ n = x ^ n
@[simp]
theorem ENNReal.rpow_ofNat (x : ENNReal) (n : ) [] :
x ^ = x ^
@[simp]
theorem ENNReal.rpow_int_cast (x : ENNReal) (n : ) :
x ^ n = x ^ n
theorem ENNReal.rpow_two (x : ENNReal) :
x ^ 2 = x ^ 2
theorem ENNReal.mul_rpow_eq_ite (x : ENNReal) (y : ENNReal) (z : ) :
(x * y) ^ z = if (x = 0 y = x = y = 0) z < 0 then else x ^ z * y ^ z
theorem ENNReal.mul_rpow_of_ne_top {x : ENNReal} {y : ENNReal} (hx : x ) (hy : y ) (z : ) :
(x * y) ^ z = x ^ z * y ^ z
theorem ENNReal.coe_mul_rpow (x : NNReal) (y : NNReal) (z : ) :
(x * y) ^ z = x ^ z * y ^ z
theorem ENNReal.prod_coe_rpow {ι : Type u_1} (s : ) (f : ιNNReal) (r : ) :
(Finset.prod s fun (i : ι) => (f i) ^ r) = (Finset.prod s fun (i : ι) => f i) ^ r
theorem ENNReal.mul_rpow_of_ne_zero {x : ENNReal} {y : ENNReal} (hx : x 0) (hy : y 0) (z : ) :
(x * y) ^ z = x ^ z * y ^ z
theorem ENNReal.mul_rpow_of_nonneg (x : ENNReal) (y : ENNReal) {z : } (hz : 0 z) :
(x * y) ^ z = x ^ z * y ^ z
theorem ENNReal.prod_rpow_of_ne_top {ι : Type u_1} {s : } {f : ιENNReal} (hf : is, f i ) (r : ) :
(Finset.prod s fun (i : ι) => f i ^ r) = (Finset.prod s fun (i : ι) => f i) ^ r
theorem ENNReal.prod_rpow_of_nonneg {ι : Type u_1} {s : } {f : ιENNReal} {r : } (hr : 0 r) :
(Finset.prod s fun (i : ι) => f i ^ r) = (Finset.prod s fun (i : ι) => f i) ^ r
theorem ENNReal.inv_rpow (x : ENNReal) (y : ) :
x⁻¹ ^ y = (x ^ y)⁻¹
theorem ENNReal.div_rpow_of_nonneg (x : ENNReal) (y : ENNReal) {z : } (hz : 0 z) :
(x / y) ^ z = x ^ z / y ^ z
theorem ENNReal.strictMono_rpow_of_pos {z : } (h : 0 < z) :
StrictMono fun (x : ENNReal) => x ^ z
theorem ENNReal.monotone_rpow_of_nonneg {z : } (h : 0 z) :
Monotone fun (x : ENNReal) => x ^ z
@[simp]
theorem ENNReal.orderIsoRpow_apply (y : ) (hy : 0 < y) (x : ENNReal) :
() x = x ^ y
def ENNReal.orderIsoRpow (y : ) (hy : 0 < y) :

Bundles fun x : ℝ≥0∞ => x ^ y into an order isomorphism when y : ℝ is positive, where the inverse is fun x : ℝ≥0∞ => x ^ (1 / y).

Equations
Instances For
theorem ENNReal.orderIsoRpow_symm_apply (y : ) (hy : 0 < y) :
theorem ENNReal.rpow_le_rpow {x : ENNReal} {y : ENNReal} {z : } (h₁ : x y) (h₂ : 0 z) :
x ^ z y ^ z
theorem ENNReal.rpow_lt_rpow {x : ENNReal} {y : ENNReal} {z : } (h₁ : x < y) (h₂ : 0 < z) :
x ^ z < y ^ z
theorem ENNReal.rpow_le_rpow_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
x ^ z y ^ z x y
theorem ENNReal.rpow_lt_rpow_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
x ^ z < y ^ z x < y
theorem ENNReal.le_rpow_one_div_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
x y ^ (1 / z) x ^ z y
theorem ENNReal.lt_rpow_one_div_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
x < y ^ (1 / z) x ^ z < y
theorem ENNReal.rpow_one_div_le_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
x ^ (1 / z) y x y ^ z
theorem ENNReal.rpow_lt_rpow_of_exponent_lt {x : ENNReal} {y : } {z : } (hx : 1 < x) (hx' : x ) (hyz : y < z) :
x ^ y < x ^ z
theorem ENNReal.rpow_le_rpow_of_exponent_le {x : ENNReal} {y : } {z : } (hx : 1 x) (hyz : y z) :
x ^ y x ^ z
theorem ENNReal.rpow_lt_rpow_of_exponent_gt {x : ENNReal} {y : } {z : } (hx0 : 0 < x) (hx1 : x < 1) (hyz : z < y) :
x ^ y < x ^ z
theorem ENNReal.rpow_le_rpow_of_exponent_ge {x : ENNReal} {y : } {z : } (hx1 : x 1) (hyz : z y) :
x ^ y x ^ z
theorem ENNReal.rpow_le_self_of_le_one {x : ENNReal} {z : } (hx : x 1) (h_one_le : 1 z) :
x ^ z x
theorem ENNReal.le_rpow_self_of_one_le {x : ENNReal} {z : } (hx : 1 x) (h_one_le : 1 z) :
x x ^ z
theorem ENNReal.rpow_pos_of_nonneg {p : } {x : ENNReal} (hx_pos : 0 < x) (hp_nonneg : 0 p) :
0 < x ^ p
theorem ENNReal.rpow_pos {p : } {x : ENNReal} (hx_pos : 0 < x) (hx_ne_top : x ) :
0 < x ^ p
theorem ENNReal.rpow_lt_one {x : ENNReal} {z : } (hx : x < 1) (hz : 0 < z) :
x ^ z < 1
theorem ENNReal.rpow_le_one {x : ENNReal} {z : } (hx : x 1) (hz : 0 z) :
x ^ z 1
theorem ENNReal.rpow_lt_one_of_one_lt_of_neg {x : ENNReal} {z : } (hx : 1 < x) (hz : z < 0) :
x ^ z < 1
theorem ENNReal.rpow_le_one_of_one_le_of_neg {x : ENNReal} {z : } (hx : 1 x) (hz : z < 0) :
x ^ z 1
theorem ENNReal.one_lt_rpow {x : ENNReal} {z : } (hx : 1 < x) (hz : 0 < z) :
1 < x ^ z
theorem ENNReal.one_le_rpow {x : ENNReal} {z : } (hx : 1 x) (hz : 0 < z) :
1 x ^ z
theorem ENNReal.one_lt_rpow_of_pos_of_lt_one_of_neg {x : ENNReal} {z : } (hx1 : 0 < x) (hx2 : x < 1) (hz : z < 0) :
1 < x ^ z
theorem ENNReal.one_le_rpow_of_pos_of_le_one_of_neg {x : ENNReal} {z : } (hx1 : 0 < x) (hx2 : x 1) (hz : z < 0) :
1 x ^ z
theorem ENNReal.toNNReal_rpow (x : ENNReal) (z : ) :
x.toNNReal ^ z = (x ^ z).toNNReal
theorem ENNReal.toReal_rpow (x : ENNReal) (z : ) :
x.toReal ^ z = (x ^ z).toReal
theorem ENNReal.ofReal_rpow_of_pos {x : } {p : } (hx_pos : 0 < x) :
theorem ENNReal.ofReal_rpow_of_nonneg {x : } {p : } (hx_nonneg : 0 x) (hp_nonneg : 0 p) :
@[simp]
theorem ENNReal.rpow_rpow_inv {y : } (hy : y 0) (x : ENNReal) :
(x ^ y) ^ y⁻¹ = x
@[simp]
theorem ENNReal.rpow_inv_rpow {y : } (hy : y 0) (x : ENNReal) :
(x ^ y⁻¹) ^ y = x
theorem ENNReal.pow_rpow_inv_natCast {n : } (hn : n 0) (x : ENNReal) :
(x ^ n) ^ (n)⁻¹ = x
theorem ENNReal.rpow_inv_natCast_pow {n : } (hn : n 0) (x : ENNReal) :
(x ^ (n)⁻¹) ^ n = x
theorem ENNReal.rpow_natCast_mul (x : ENNReal) (n : ) (z : ) :
x ^ (n * z) = (x ^ n) ^ z
theorem ENNReal.rpow_mul_natCast (x : ENNReal) (y : ) (n : ) :
x ^ (y * n) = (x ^ y) ^ n
theorem ENNReal.rpow_intCast_mul (x : ENNReal) (n : ) (z : ) :
x ^ (n * z) = (x ^ n) ^ z
theorem ENNReal.rpow_mul_intCast (x : ENNReal) (y : ) (n : ) :
x ^ (y * n) = (x ^ y) ^ n
theorem ENNReal.rpow_left_injective {x : } (hx : x 0) :
Function.Injective fun (y : ENNReal) => y ^ x
theorem ENNReal.rpow_left_surjective {x : } (hx : x 0) :
Function.Surjective fun (y : ENNReal) => y ^ x
theorem ENNReal.rpow_left_bijective {x : } (hx : x 0) :
Function.Bijective fun (y : ENNReal) => y ^ x