Powers of extended natural numbers

We define the power of an extended natural x : ℕ∞ by another extended natural y : ℕ∞. The definition is chosen such that x ^ y is the cardinality of α → β, when β has cardinality x and α has cardinality y:

• When y is finite, it coincides with the exponentiation by natural numbers (e.g. ⊤ ^ 0 = 1).
• We set 0 ^ ⊤ = 0, 1 ^ ⊤ = 1 and x ^ ⊤ = ⊤ for x > 1.

Naming convention

The quantity x ^ y for x, y : ℕ∞ is defined as a Pow instance. It is called epow in lemmas' names.

instance ENat.instPow : Pow ℕ∞ ℕ∞

Equations

• ENat.instPow = { pow := fun (x x_1 : ℕ∞) => match x, x_1 with | x, some y => x ^ y | x, none => if x = 0 then 0 else if x = 1 then 1 else ⊤ }

@[simp]

theorem ENat.epow_natCast {x : ℕ∞} {y : ℕ} : x ^ ↑y = x ^ y

@[simp]

theorem ENat.zero_epow_top : 0 ^ ⊤ = 0

theorem ENat.zero_epow {y : ℕ∞} (h : y ≠ 0) : 0 ^ y = 0

@[simp]

theorem ENat.one_epow {y : ℕ∞} : 1 ^ y = 1

@[simp]

theorem ENat.top_epow_top : ⊤ ^ ⊤ = ⊤

theorem ENat.top_epow {y : ℕ∞} (h : y ≠ 0) : ⊤ ^ y = ⊤

@[simp]

theorem ENat.epow_zero {x : ℕ∞} : x ^ 0 = 1

@[simp]

theorem ENat.epow_one {x : ℕ∞} : x ^ 1 = x

theorem ENat.epow_top {x : ℕ∞} (h : 1 < x) : x ^ ⊤ = ⊤

theorem ENat.epow_right_mono {x : ℕ∞} (h : x ≠ 0) : Monotone fun (y : ℕ∞) => x ^ y

theorem ENat.one_le_epow {x y : ℕ∞} (h : x ≠ 0) : 1 ≤ x ^ y

theorem ENat.epow_left_mono {y : ℕ∞} : Monotone fun (x : ℕ∞) => x ^ y

theorem ENat.epow_eq_zero_iff {x y : ℕ∞} : x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

theorem ENat.epow_eq_one_iff {x y : ℕ∞} : x ^ y = 1 ↔ x = 1 ∨ y = 0

theorem ENat.epow_add {x y z : ℕ∞} : x ^ (y + z) = x ^ y * x ^ z

theorem ENat.mul_epow {x y z : ℕ∞} : (x * y) ^ z = x ^ z * y ^ z

theorem ENat.epow_mul {x y z : ℕ∞} : x ^ (y * z) = (x ^ y) ^ z