Ordinal.principal_add_iff_zero_or_omega_opow
theorem Ordinal.principal_add_iff_zero_or_omega_opow :
∀ {o : Ordinal.{u_1}}, Ordinal.Principal (fun x x_1 => x + x_1) o ↔ o = 0 ∨ ∃ a, o = Ordinal.omega ^ a
This theorem provides the main characterization for additive principal ordinals. The theorem states that for any ordinal 'o', 'o' is an additive principal ordinal if and only if 'o' is either 0 or can be expressed as an exponential of the first infinite ordinal 'ω' raised to some ordinal 'a'. In simpler terms, an ordinal 'o' is considered additive principal if, for any pair of ordinals 'a' and 'b' less than 'o', their sum is still less than 'o', and this property holds true if 'o' is either 0 or of the form 'ω' raised to the power of some ordinal 'a'.
More concisely: An ordinal is additive principal if and only if it is 0 or of the form ω^a for some ordinal a.
|
Ordinal.principal_mul_iff_le_two_or_omega_opow_opow
theorem Ordinal.principal_mul_iff_le_two_or_omega_opow_opow :
∀ {o : Ordinal.{u_1}},
Ordinal.Principal (fun x x_1 => x * x_1) o ↔ o ≤ 2 ∨ ∃ a, o = Ordinal.omega ^ Ordinal.omega ^ a
This theorem provides a key characterization of multiplicative principal ordinals. It essentially states that for any ordinal 'o', 'o' is a multiplicative principal ordinal (i.e., the set of ordinals less than 'o' is closed under multiplication) if and only if 'o' is less than or equal to 2 or there exists an ordinal 'a' such that 'o' is equal to 'omega' to the power of ('omega' to the power of 'a'), where 'omega' represents the first infinite ordinal.
More concisely: A multiplicative principal ordinal 'o' is equivalent to 'omega' raised to some power, or is less than or equal to 2.
|
Ordinal.principal_add_isLimit
theorem Ordinal.principal_add_isLimit :
∀ {o : Ordinal.{u_1}}, 1 < o → Ordinal.Principal (fun x x_1 => x + x_1) o → o.IsLimit
The theorem `Ordinal.principal_add_isLimit` states that for any ordinal `o`, if `o` is greater than 1 and is a principal ordinal with respect to the operation of addition (meaning all ordinals less than `o`, when added together, result in an ordinal still less than `o`), then `o` is a limit ordinal. A limit ordinal, here, is defined as an ordinal which is not zero and is not the successor of any other ordinal.
More concisely: If an ordinal greater than 1 is principal with respect to addition, then it is a limit ordinal.
|
Ordinal.principal_zero
theorem Ordinal.principal_zero : ∀ {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}}, Ordinal.Principal op 0 := by
sorry
The theorem `Ordinal.principal_zero` states that for any binary operation on ordinals, the ordinal zero is considered principal. In other words, for any two ordinals that are less than zero, the result of the operation on these two ordinals is also less than zero. This is a somewhat unconventional definition, since typically the concept of a principal ordinal is used in the context of non-zero ordinals.
More concisely: The theorem `Ordinal.principal_zero` asserts that the ordinal zero is the identity element for any binary operation on ordinals, such that for all ordinals `x` and `y` below zero, `x + y` (or `x * y` for multiplication) is less than zero.
|
Ordinal.add_omega_opow
theorem Ordinal.add_omega_opow :
∀ {a b : Ordinal.{u_1}}, a < Ordinal.omega ^ b → a + Ordinal.omega ^ b = Ordinal.omega ^ b
The theorem `Ordinal.add_omega_opow` states that for any two ordinals `a` and `b`, if `a` is less than the omega ordinal raised to the power of `b` (i.e., `a < ω^b`), then the sum of `a` and `ω^b` is equal to `ω^b`. In other words, adding a smaller ordinal to `ω^b` does not change the value of `ω^b`. This result reflects the fundamental property of infinite ordinals where adding a smaller ordinal to an infinite ordinal doesn't increase the size of the infinite ordinal.
More concisely: For all ordinals `a` and `b`, if `a < ω^b`, then `a + ω^b = ω^b`.
|