Ordinal.nadd_lt_nadd_left
theorem Ordinal.nadd_lt_nadd_left : ∀ {b c : Ordinal.{u}}, b < c → ∀ (a : Ordinal.{u}), a.nadd b < a.nadd c
The theorem `Ordinal.nadd_lt_nadd_left` states that for any three ordinals `a`, `b`, and `c`, if `b` is less than `c`, then the natural addition of `a` and `b`, denoted as `Ordinal.nadd a b`, is also less than the natural addition of `a` and `c`, denoted as `Ordinal.nadd a c`. This theorem thus asserts the monotonicity of the natural addition of ordinals with respect to the second ordinal.
More concisely: For all ordinals `a`, `b`, and `c`, if `b` < `c`, then `Ordinal.nadd a b` < `Ordinal.nadd a c`.
|
Ordinal.nadd_zero
theorem Ordinal.nadd_zero : ∀ (a : Ordinal.{u}), a.nadd 0 = a
The theorem `Ordinal.nadd_zero` states that for any ordinal number `a`, the natural addition (also known as the Hessenberg sum) of `a` and zero is `a`. This means when you add zero, using the natural addition operation defined for ordinal numbers, to any ordinal number, the result will be the original ordinal number.
More concisely: For any ordinal number `a`, `a + 0 = a`.
|
Ordinal.lt_nadd_iff
theorem Ordinal.lt_nadd_iff :
∀ {a b c : Ordinal.{u}}, a < b.nadd c ↔ (∃ b' < b, a ≤ b'.nadd c) ∨ ∃ c' < c, a ≤ b.nadd c'
This theorem establishes a property of the natural addition (also known as the Hessenberg sum) operation on ordinals. For any three ordinals `a`, `b`, and `c`, it states that `a` is less than the natural addition of `b` and `c` if and only if there exists an ordinal `b'` less than `b` such that `a` is less than or equal to the natural addition of `b'` and `c`, or there exists an ordinal `c'` less than `c` such that `a` is less than or equal to the natural addition of `b` and `c'`. This theorem essentially explains the recursive definition of the Hessenberg sum by identifying the conditions under which one ordinal is less than the Hessenberg sum of two others.
More concisely: For any ordinals `a`, `b`, and `c`, `a` is less than `b + c` if and only if there exists an ordinal `b' < b` such that `a <= b' + c` or there exists an ordinal `c' < c` such that `a <= b + c'`.
|
Ordinal.nmul_nonempty
theorem Ordinal.nmul_nonempty :
∀ (a b : Ordinal.{u}), {c | ∀ a' < a, ∀ b' < b, (a'.nmul b).nadd (a.nmul b') < c.nadd (a'.nmul b')}.Nonempty := by
sorry
The theorem `Ordinal.nmul_nonempty` asserts that for every pair of ordinals `a` and `b`, there exists an ordinal `c` such that for all `a'` less than `a` and `b'` less than `b`, the result of the operation `a'.nmul b` added to `a.nmul b'` is less than `c` added to `a'.nmul b'`. Here, `nmul` and `nadd` stand for multiplication and addition of ordinals, respectively. This asserts a form of consistency between ordinal addition and multiplication.
More concisely: For all ordinals `a` and `b`, there exists an ordinal `c` such that for all `a'
|
Ordinal.zero_nadd
theorem Ordinal.zero_nadd : ∀ (a : Ordinal.{u}), Ordinal.nadd 0 a = a
The theorem `Ordinal.zero_nadd` states that for any ordinal `a` from the type of well orders, the natural addition (also known as the Hessenberg sum) of 0 and `a` is equal to `a`. This is akin to the identity property in arithmetic where adding zero to any number does not change its value.
More concisely: For any ordinal `a`, `0 + a = a`.
|
Ordinal.nadd_le_nadd_right
theorem Ordinal.nadd_le_nadd_right : ∀ {b c : Ordinal.{u}}, b ≤ c → ∀ (a : Ordinal.{u}), b.nadd a ≤ c.nadd a
The theorem `Ordinal.nadd_le_nadd_right` states that for any ordinals `b` and `c`, if `b` is less than or equal to `c`, then for any ordinal `a`, the natural addition of `b` and `a` (denoted by `Ordinal.nadd b a`) is less than or equal to the natural addition of `c` and `a` (denoted by `Ordinal.nadd c a`). This theorem essentially shows that the natural addition operation on ordinals respects the order relation, i.e., if one operand is smaller, the result of the operation is also smaller, when the other operand is fixed.
More concisely: For all ordinals `b` and `c` and any ordinal `a`, if `b ≤ c`, then `Ordinal.nadd b a ≤ Ordinal.nadd c a`.
|
NatOrdinal.induction
theorem NatOrdinal.induction :
∀ {p : NatOrdinal → Prop} (i : NatOrdinal), (∀ (j : NatOrdinal), (∀ k < j, p k) → p j) → p i
This theorem, `NatOrdinal.induction`, is essentially a version of the principle of mathematical induction but specialized to `NatOrdinal`, a type synonym for ordinals with natural addition and multiplication. It asserts that for any property `p` and any ordinal `i` (both of the type `NatOrdinal`), if for every ordinal `j`, the truth of `p` for all ordinals `k` less than `j` implies the truth of `p` for `j`, then `p` holds for `i`. In other words, it is the basic principle of induction applied to the natural ordinals.
More concisely: If for all ordinals `j` in `NatOrdinal`, if `p` holds for all ordinals `k` less than `j`, then `p` holds for `j`, then `p` holds for the given ordinal `i` in `NatOrdinal`. (This is the principle of mathematical induction specialized to natural ordinals.)
|
Ordinal.nadd_def
theorem Ordinal.nadd_def :
∀ (a b : Ordinal.{u}), a.nadd b = max (a.blsub fun a' x => a'.nadd b) (b.blsub fun b' x => a.nadd b')
The theorem `Ordinal.nadd_def` states that for any two ordinals `a` and `b`, the natural addition of `a` and `b` (denoted as `Ordinal.nadd a b`), also known as the Hessenberg sum, is equal to the maximum of two values. The first value is the least strict upper bound of the family of ordinals obtained by performing natural addition of `b` and each ordinal less than `a`. The second value is similarly defined, but with the roles of `a` and `b` swapped, i.e., it is the least strict upper bound of the family of ordinals obtained by performing natural addition of `a` and each ordinal less than `b`.
More concisely: The theorem `Ordinal.nadd_def` asserts that for all ordinals `a` and `b`, `Ordinal.nadd a b` equals the least upper bound of the set `{a + b | x < a} ∪ {a + b | x < b}`.
|
Ordinal.nadd_comm
theorem Ordinal.nadd_comm : ∀ (a b : Ordinal.{u_1}), a.nadd b = b.nadd a
This theorem states that natural addition, denoted as `Ordinal.nadd`, on ordinals is commutative. In other words, for any two ordinals `a` and `b`, the ordinal resulting from performing the natural addition of `a` and `b` is the same as the ordinal resulting from performing natural addition of `b` and `a`. This characteristic is in contrast to normal ordinal addition, therefore, emphasizing the property of natural addition being commutative.
More concisely: For all ordinals a and b, `Ordinal.nadd a b = Ordinal.nadd b a`.
|
Ordinal.nadd_le_nadd_left
theorem Ordinal.nadd_le_nadd_left : ∀ {b c : Ordinal.{u}}, b ≤ c → ∀ (a : Ordinal.{u}), a.nadd b ≤ a.nadd c
The theorem `Ordinal.nadd_le_nadd_left` states that for any ordinals `b` and `c` in a given type, if `b` is less than or equal to `c`, then for any ordinal `a`, the natural addition of `a` and `b` (denoted as `Ordinal.nadd a b`) is less than or equal to the natural addition of `a` and `c` (denoted as `Ordinal.nadd a c`). In other words, if an ordinal `b` is less than or equal to an ordinal `c`, then adding any ordinal `a` to `b` naturally will always result in an ordinal that is less than or equal to the ordinal resulting from naturally adding `a` to `c`. This shows a property of monotonicity in the natural addition of ordinals.
More concisely: For all ordinals `a`, `b`, and `c`, if `b` is less than or equal to `c`, then `Ordinal.nadd a b` is less than or equal to `Ordinal.nadd a c`.
|
Ordinal.nmul_zero
theorem Ordinal.nmul_zero : ∀ (a : Ordinal.{u_1}), a.nmul 0 = 0
This theorem states that for any ordinal `a` in some type `u_1`, the "multiplication by natural numbers" operation (denoted here as `Ordinal.nmul`) with `a` and the ordinal `0` yields `0`. In other words, multiplying any ordinal number by zero yields zero, mimicking the familiar property in arithmetic.
More concisely: For any ordinal `a`, `a * 0 = 0`.
|
Ordinal.nadd_one
theorem Ordinal.nadd_one : ∀ (a : Ordinal.{u}), a.nadd 1 = Order.succ a
This theorem states that for every ordinal `a`, the natural addition of `a` and the ordinal `1` is equivalent to the successor of `a`. In other words, it asserts that when you apply the Hessenberg sum operation (which is the specific form of addition defined for ordinals) with `a` and `1`, you get the next ordinal in the order, which is what `Order.succ a` represents. This holds true for all ordinals `a`.
More concisely: For every ordinal `a`, the Hessenberg sum of `a` and `1` equals `Order.succ a`.
|
Ordinal.zero_nmul
theorem Ordinal.zero_nmul : ∀ (a : Ordinal.{u_1}), Ordinal.nmul 0 a = 0
The theorem `Ordinal.zero_nmul` states that for any ordinal number `a`, the natural number multiplication of zero and `a` is zero. In other words, multiplying any ordinal number by zero results in the ordinal zero.
More concisely: For any ordinal number `a`, `0 * a = 0` holds as an equality of ordinal numbers.
|
Ordinal.nmul_comm
theorem Ordinal.nmul_comm : ∀ (a b : Ordinal.{u_1}), a.nmul b = b.nmul a
The theorem `Ordinal.nmul_comm` states that for any two ordinal numbers `a` and `b`, the operation of `nmul`, or natural multiplication, is commutative. In other words, multiplying `a` and `b` in either order will yield the same result: `Ordinal.nmul a b` is equal to `Ordinal.nmul b a`.
More concisely: For all ordinal numbers `a` and `b`, `Ordinal.nmul a b` equals `Ordinal.nmul b a`.
|
Ordinal.nmul_nadd_lt
theorem Ordinal.nmul_nadd_lt :
∀ {a b a' b' : Ordinal.{u}}, a' < a → b' < b → (a'.nmul b).nadd (a.nmul b') < (a.nmul b).nadd (a'.nmul b') := by
sorry
This theorem states that for any four ordinals `a`, `b`, `a'`, and `b'`, where `a'` is less than `a` and `b'` is less than `b`, the ordinal resulting from performing a "natural addition" (also known as the Hessenberg sum) on the "natural multiplications" of `a'` and `b` and of `a` and `b'` is less than the ordinal resulting from the "natural addition" of the "natural multiplications" of `a` and `b` and of `a'` and `b'`.
More concisely: For any ordinals `a`, `b`, `a'`, and `b'` with `a' < a` and `b' < b`, we have `(a' * b) + (a * b')` < `(a * b) + (a' * b')`.
|