Ordinal.opow_zero
theorem Ordinal.opow_zero : ∀ (a : Ordinal.{u_1}), a ^ 0 = 1
This theorem states that for any ordinal number 'a', if you raise 'a' to the power of zero, the result is always 1. This follows the general principle in mathematics that any non-zero number raised to the power of zero equals 1. In this context, the theorem applies to ordinal numbers, which are a type of well orders in a given type, up to order isomorphism.
More concisely: For any ordinal number 'a', a^0 = 1.
|
Mathlib.SetTheory.Ordinal.Exponential._auxLemma.5
theorem Mathlib.SetTheory.Ordinal.Exponential._auxLemma.5 :
∀ {α : Type u} [inst : Preorder α] (a : α), (a ≤ a) = True
This theorem states that for any type `α` under a preorder, every element `a` of type `α` is less than or equal to itself. In mathematical terms, for all `a` in some set that is preordered, the statement `a ≤ a` is always true. This property is known as reflexivity, a fundamental aspect of preorders.
More concisely: In any preorder, every element is refundlexive, i.e., for all `a`, `a ≤ a`.
|
Ordinal.log_zero_left
theorem Ordinal.log_zero_left : ∀ (b : Ordinal.{u_1}), Ordinal.log 0 b = 0
The theorem `Ordinal.log_zero_left` states that for any ordinal number `b`, the ordinal logarithm of `0` base `b` is always `0`. This is very similar to the rule in basic arithmetic that anything raised to the power of `0` is `1`, except that in the setting of ordinal numbers, the base `0` logarithm of any number is `0`.
More concisely: For any ordinal number `b`, the ordinal logarithm of `0` base `b` equals `0`.
|
Ordinal.opow_ne_zero
theorem Ordinal.opow_ne_zero : ∀ {a : Ordinal.{u_1}} (b : Ordinal.{u_1}), a ≠ 0 → a ^ b ≠ 0
The theorem `Ordinal.opow_ne_zero` states that for any two ordinals `a` and `b` in the same type `u_1`, if `a` is not equal to zero, then `a` raised to the power `b` (`a ^ b`) is also not equal to zero. Here, `Ordinal` refers to the type of well-ordered sets up to order isomorphism in a certain type. This is a fact about exponentiation in the context of ordinals: a non-zero ordinal raised to any ordinal power is always non-zero.
More concisely: For any ordinals `a` and `b` in the same type `u_1` with `a` non-zero, `a^b` is also non-zero.
|
Ordinal.opow_le_opow_iff_right
theorem Ordinal.opow_le_opow_iff_right : ∀ {a b c : Ordinal.{u_1}}, 1 < a → (a ^ b ≤ a ^ c ↔ b ≤ c)
This theorem states that for any three ordinals `a`, `b`, and `c` in a type `u_1`, assuming `a` is greater than 1, the ordinal exponentiation `a` raised to the power `b` is less than or equal to `a` raised to the power `c` if and only if `b` is less than or equal to `c`. This essentially states the property of increasing monotonicity of the exponentiation function for ordinals greater than 1.
More concisely: For ordinals `a` > 1, `a^b` <= `a^c` if and only if `b` <= `c`.
|
Ordinal.opow_one_add
theorem Ordinal.opow_one_add : ∀ (a b : Ordinal.{u_1}), a ^ (1 + b) = a * a ^ b
This theorem states that for any two well-orders `a` and `b` in a given type `Type u_1`, the ordinal exponentiation of `a` to the power of `1 + b` is equal to `a` times the ordinal exponentiation of `a` to the power of `b`. In other words, it's asserting the property similar to the law of exponents $(a^{1+b} = a*a^{b})$ but in the context of ordinals.
More concisely: For any ordinals `a` and `b`, `a ^ (1 + b) = a ^ b * a`.
|
Ordinal.opow_succ
theorem Ordinal.opow_succ : ∀ (a b : Ordinal.{u_1}), a ^ Order.succ b = a ^ b * a
The theorem `Ordinal.opow_succ` states that for any two ordinals `a` and `b`, the ordinal exponentiation of `a` to the successor of `b` (i.e., `a ^ Order.succ b`) equals the result of multiplying `a` to the power of `b` by `a` (i.e., `a ^ b * a`). This is similar to the basic property of exponentiation in elementary mathematics where `a` to the power of `n+1` is equal to `a` to the power of `n` times `a`.
More concisely: For any ordinals `a` and `b`, `a^(Order.succ b)` equals `a^b * a`.
|
Mathlib.SetTheory.Ordinal.Exponential._auxLemma.6
theorem Mathlib.SetTheory.Ordinal.Exponential._auxLemma.6 : ∀ (o : Ordinal.{u_3}), (0 ≤ o) = True
The theorem `Mathlib.SetTheory.Ordinal.Exponential._auxLemma.6` states that for every ordinal `o`, the property that `o` is greater than or equal to zero is always true. In other words, it asserts that no ordinal can be less than zero. This is analogous to the property of natural numbers in mathematics where every natural number is non-negative.
More concisely: Every ordinal is non-negative.
|
Ordinal.opow_one
theorem Ordinal.opow_one : ∀ (a : Ordinal.{u_1}), a ^ 1 = a
This theorem states that for any ordinal number `a`, raising `a` to the power of 1 is equivalent to `a` itself. In the context of the theory of ordinal numbers in set theory, this means that the single exponentiation of any ordinal number does not modify its value, analogy to the property from basic arithmetic that any number raised to the power of 1 stays the same.
More concisely: For any ordinal number `a`, `a^1 = a`.
|
Ordinal.opow_lt_opow_iff_right
theorem Ordinal.opow_lt_opow_iff_right : ∀ {a b c : Ordinal.{u_1}}, 1 < a → (a ^ b < a ^ c ↔ b < c)
This theorem states that for any three ordinals `a`, `b`, and `c`, if `a` is greater than 1, then `a` raised to the power of `b` is less than `a` raised to the power of `c` if and only if `b` is less than `c`. In other words, it illustrates the monotonicity of the exponentiation operation in the context of ordinals when the base ordinal is greater than 1.
More concisely: For ordinals `a` > 1, `a^b` < `a^c` if and only if `b` < `c`.
|
Ordinal.one_opow
theorem Ordinal.one_opow : ∀ (a : Ordinal.{u_1}), 1 ^ a = 1
The theorem `Ordinal.one_opow` states that for any ordinal `a`, the ordinal exponentiation of `1` to the power `a` is always `1`. In other words, regardless of the ordinal `a`, when `1` is raised to any ordinal power, the result is always `1`. This is analogous to the rule in conventional mathematics where any number raised to the power of zero is one, and here it is generalized to ordinals.
More concisely: For any ordinal `a`, the ordinal exponentiation `1^a` equals `1`.
|
Ordinal.log_of_not_one_lt_left
theorem Ordinal.log_of_not_one_lt_left : ∀ {b : Ordinal.{u_1}}, ¬1 < b → ∀ (x : Ordinal.{u_1}), b.log x = 0
The theorem `Ordinal.log_of_not_one_lt_left` states that for any ordinals `b` and `x`, if `b` is not greater than 1 then the ordinal logarithm of `x` with base `b` is equal to 0. In other words, when the base of the ordinal logarithm is not greater than 1, the ordinal logarithm always returns 0 regardless of the value of `x`. This theorem is a reflection of the mathematical fact that logarithms are undefined for bases less than or equal to 1.
More concisely: For any ordinal `b` less than or equal to 1 and any ordinal `x`, the ordinal logarithm of `x` with base `b` equals 0.
|
Ordinal.lt_opow_of_limit
theorem Ordinal.lt_opow_of_limit : ∀ {a b c : Ordinal.{u_1}}, b ≠ 0 → c.IsLimit → (a < b ^ c ↔ ∃ c' < c, a < b ^ c')
This theorem, `Ordinal.lt_opow_of_limit`, states that for any three ordinals `a`, `b`, and `c`, where `b` is not zero and `c` is a limit ordinal, `a` is less than `b` to the power `c` if and only if there exists an ordinal `c'` less than `c` such that `a` is less than `b` to the power `c'`. The power operation here is ordinal exponentiation.
More concisely: For any ordinals `a`, `b`, and limit ordinal `c` with `b > 0`, `a < b^c` if and only if there exists an ordinal `c' < c` such that `a < b^c'`.
|
Ordinal.lt_opow_succ_log_self
theorem Ordinal.lt_opow_succ_log_self :
∀ {b : Ordinal.{u_1}}, 1 < b → ∀ (x : Ordinal.{u_1}), x < b ^ Order.succ (b.log x)
This theorem states that for any ordinal `b` such that `1 < b` and any ordinal `x`, the value of `x` is strictly less than `b` raised to the power of the successor of the ordinal logarithm of `x` base `b`. In mathematical terms, for all `b` and `x` where `b` is an ordinal greater than `1`, we have `x < b^((Ordinal.log b x)+1)`. The ordinal logarithm here is a solution `u` to the equation `x = b ^ u * v + w` where `v < b` and `w < b ^ u`. The successor of an ordinal is the least ordinal greater than it if it is not maximal, or the ordinal itself if it is maximal. This theorem could be important in the proof of properties related to ordinal arithmetic and logarithms.
More concisely: For any ordinal `b` greater than 1 and any ordinal `x`, `x` is strictly less than `b` raised to the power of the successor of the ordinal logarithm of `x` base `b`.
|
Ordinal.succ_log_def
theorem Ordinal.succ_log_def : ∀ {b x : Ordinal.{u_1}}, 1 < b → x ≠ 0 → Order.succ (b.log x) = sInf {o | x < b ^ o}
The theorem `Ordinal.succ_log_def` states that for any two ordinals `b` and `x` such that `b` is greater than 1 and `x` is not equal to zero, the successor of the ordinal logarithm of `x` with base `b` is equal to the least ordinal `o` for which `x` is less than `b` raised to the power `o`. This theorem provides a relation between the successor of an ordinal logarithm and the set of ordinals satisfying a certain inequality.
More concisely: For any ordinal `x` not equal to zero and base `b` greater than 1, the successor of the ordinal logarithm of `x` with base `b` equals the least ordinal `o` such that `x` is below `b^o`.
|
Ordinal.log_zero_right
theorem Ordinal.log_zero_right : ∀ (b : Ordinal.{u_1}), b.log 0 = 0
The theorem `Ordinal.log_zero_right` states that for any ordinal `b`, the ordinal logarithm of `0` base `b` is `0`. In other words, in the context of ordinals, the logarithm of `0` to any base is `0`, similar to how the logarithm of `1` to any base is `0` in real numbers.
More concisely: For any ordinal `b`, the ordinal logarithm of `0` base `b` equals `0`.
|
Ordinal.opow_le_opow_right
theorem Ordinal.opow_le_opow_right : ∀ {a b c : Ordinal.{u_1}}, 0 < a → b ≤ c → a ^ b ≤ a ^ c
The theorem `Ordinal.opow_le_opow_right` states that for all ordinals `a`, `b`, and `c` in a given type, if `a` is greater than 0 and `b` is less than or equal to `c`, then `a` raised to the power `b` is less than or equal to `a` raised to the power `c`. This property can be seen as an extension of the monotonicity of the exponentiation function to the context of ordinals.
More concisely: For all ordinals `a`, `b`, and `c` with `a > 0` and `b <= c`, we have `a^b <= a^c`.
|
Ordinal.opow_log_le_self
theorem Ordinal.opow_log_le_self : ∀ (b : Ordinal.{u_1}) {x : Ordinal.{u_1}}, x ≠ 0 → b ^ b.log x ≤ x
The theorem `Ordinal.opow_log_le_self` states that for any ordinal number `b` and any non-zero ordinal `x`, raising `b` to the power of the ordinal logarithm of `x` with base `b` (`b` to the power of `Ordinal.log b x`) is less than or equal to `x`. In other words, it's stating that the ordinal logarithm is a kind of upper bound on the power to which you can raise `b` without exceeding `x`.
More concisely: For any non-zero ordinal number `x` and base `b`, the ordinal logarithm of `x` with base `b` (`Ordinal.log b x`) satisfies `b^(Ordinal.log b x) ≤ x`.
|
Ordinal.opow_isNormal
theorem Ordinal.opow_isNormal : ∀ {a : Ordinal.{u_1}}, 1 < a → Ordinal.IsNormal fun x => a ^ x
The theorem `Ordinal.opow_isNormal` states that for any ordinal `a` such that `a` is greater than 1, the function `f` defined as `f(x) = a^x` is a normal ordinal function. A normal ordinal function is a function that is strictly increasing (i.e., for any ordinal `o`, `f(o)` is less than `f` of the successor of `o`) and is order-continuous (i.e., for any limit ordinal `o`, the image `f(o)` is the supremum of `f(a)` for all `a` that are less than `o`).
More concisely: For any ordinal `a` greater than 1, the function `f(x) = a^x` is a normal ordinal function. (i.e., it is strictly increasing and order-continuous).
|
Ordinal.opow_le_iff_le_log
theorem Ordinal.opow_le_iff_le_log : ∀ {b x c : Ordinal.{u_1}}, 1 < b → x ≠ 0 → (b ^ c ≤ x ↔ c ≤ b.log x)
The theorem `Ordinal.opow_le_iff_le_log` establishes a type of almost-Galois connection between the ordinal exponentiation function (`opow`) and the ordinal logarithm function (`log`). Specifically, for any three ordinals `b`, `x`, and `c`, where `b` is greater than 1 and `x` is not zero, the theorem states that `b` raised to the power of `c` is less than or equal to `x` if and only if `c` is less than or equal to the ordinal logarithm of `x` with base `b`. In other words, the ordinal exponentiation and logarithm functions inversely relate to each other in terms of ordering.
More concisely: For any ordinals $b > 1$, $x \neq 0$, and $c$, the equality $b^c \leq x$ holds if and only if $c \leq \log_b x$.
|
Ordinal.opow_pos
theorem Ordinal.opow_pos : ∀ {a : Ordinal.{u_1}} (b : Ordinal.{u_1}), 0 < a → 0 < a ^ b
The theorem `Ordinal.opow_pos` states that for any two ordinals `a` and `b`, if `a` is greater than 0, then `a` raised to the power of `b` is also greater than 0. In mathematical terms, this theorem is stating that for any two ordinal numbers `a` and `b`, if `a > 0` then `a^b > 0`. This is essentially a property of ordinal exponentiation, guaranteeing that a positive base results in a positive result when raised to any power.
More concisely: For any ordinal numbers `a` and `b` with `a > 0`, `a^b > 0`.
|
Ordinal.zero_opow
theorem Ordinal.zero_opow : ∀ {a : Ordinal.{u_1}}, a ≠ 0 → 0 ^ a = 0
The theorem `Ordinal.zero_opow` states that for any ordinal `a` that is not equal to zero, the ordinal exponentiation of zero to the power of `a` is equal to zero. In other words, raising zero to the power of any non-zero ordinal results in zero.
This is reflected in the standard arithmetic where any non-zero number raised to the power of zero is 1, but zero raised to the power of any non-zero number is still zero.
More concisely: For any non-zero ordinal `a`, `0^a = 0`.
|
Ordinal.log_nonempty
theorem Ordinal.log_nonempty : ∀ {b x : Ordinal.{u_1}}, 1 < b → {o | x < b ^ o}.Nonempty
This theorem states that for any two ordinals `b` and `x` in the same universe `u_1`, as long as `b` is greater than 1, there exists an ordinal `o` such that `x` is less than `b` raised to the power of `o`. In other words, the set of all `o` for which `x` is less than `b` to the power of `o` is always nonempty when `b` is larger than 1.
More concisely: For any ordinal `b` greater than 1 and any ordinal `x` in the same universe, there exists an ordinal `o` such that `x` is below `b` raised to the power `o`.
|
Ordinal.right_le_opow
theorem Ordinal.right_le_opow : ∀ {a : Ordinal.{u_1}} (b : Ordinal.{u_1}), 1 < a → b ≤ a ^ b
The theorem `Ordinal.right_le_opow` states that for any well-ordered set `a` and any well-ordered set `b`, if `a` is strictly greater than 1, then `b` is less than or equal to `a` raised to the power `b`. This theorem is defined for well-ordered sets in the same universe `u_1`.
More concisely: For any well-ordered sets `a` in universe `u_1` with `a > 1` and `b` in the same universe, `b` is less than or equal to `a^b`.
|
Ordinal.opow_add
theorem Ordinal.opow_add : ∀ (a b c : Ordinal.{u_1}), a ^ (b + c) = a ^ b * a ^ c
The theorem `Ordinal.opow_add` states that for any three well-ordered sets `a`, `b`, and `c` in a given type, the ordinal exponentiation of `a` to the power of the ordinal sum of `b` and `c` is equal to the product of the ordinal exponentiation of `a` to the power of `b` and the ordinal exponentiation of `a` to the power of `c`. This theorem essentially illustrates the law of exponents for ordinal numbers, similar to that in regular arithmetic: $a^{(b + c)} = a^b * a^c$.
More concisely: For any well-ordered sets $a$, $b$, and $c$, $a^{b + c} = a^b \times a^c$ (ordinal exponentiation).
|
Ordinal.opow_le_of_limit
theorem Ordinal.opow_le_of_limit : ∀ {a b c : Ordinal.{u_1}}, a ≠ 0 → b.IsLimit → (a ^ b ≤ c ↔ ∀ b' < b, a ^ b' ≤ c)
This theorem, `Ordinal.opow_le_of_limit`, states that for any three ordinals `a`, `b`, and `c`, if `a` is not zero and `b` is a limit ordinal (i.e., an ordinal which is not zero and not a successor), then `a` raised to the power `b` is less than or equal to `c` if and only if for every ordinal `b'` less than `b`, `a` raised to the power `b'` is less than or equal to `c`. In other words, it formalizes a property of exponentiation for limit ordinals in the theory of well orders.
More concisely: For any ordinals `a` non-zero, and `b` a limit ordinal, `a^b ≤ c` if and only if for all `b' < b`, `a^(b') ≤ c`.
|