LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.SetTheory.Ordinal.Arithmetic

`Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.10` theorem Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.10 : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, (¬a ≤ b) = (b < a) This theorem from the Set Theory Ordinal Arithmetic in Mathlib library states that for any type `α` that has a `LinearOrder` instance, and for any two elements `a` and `b` of that type, the statement that `a` is not less than or equal to `b` is equivalent to the statement that `b` is strictly less than `a`. This is a basic property of ordered sets. More concisely: In an ordered set, for all elements `a` and `b`, `a` is not less than or equal to `b` if and only if `b` is strictly less than `a`.
`Ordinal.enumOrd_surjective` theorem Ordinal.enumOrd_surjective : ∀ {S : Set Ordinal.{u}}, Set.Unbounded (fun x x_1 => x < x_1) S → ∀ s ∈ S, ∃ a, Ordinal.enumOrd S a = s The theorem `Ordinal.enumOrd_surjective` states that for any unbounded set `S` of ordinals, where 'unbounded' is defined in terms of the strict less than relation (`<`), for every ordinal `s` in `S`, there exists an ordinal `a` such that when we apply the enumerator function `Ordinal.enumOrd` to the set `S` and ordinal `a`, we obtain the ordinal `s`. In other words, every ordinal in the unbounded set `S` is within the range of the enumerator function `Ordinal.enumOrd`. More concisely: For any unbounded set `S` of ordinals, the enumerator function `Ordinal.enumOrd` is surjective over `S`.
`Ordinal.mul_le_of_limit` theorem Ordinal.mul_le_of_limit : ∀ {a b c : Ordinal.{u_4}}, b.IsLimit → (a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c) The theorem `Ordinal.mul_le_of_limit` states that for any three ordinals `a`, `b`, and `c`, if `b` is a limit ordinal, then the product `a * b` is less than or equal to `c` if and only if for all `b'` less than `b`, the product `a * b'` is less than or equal to `c`. In essence, this theorem relates the property of being a limit ordinal with the property of respecting a certain order inequality when multiplied by another ordinal. More concisely: For any ordinals `a`, `b`, and `c`, if `b` is a limit ordinal, then `a b <= c` if and only if `a * b' <= c` for all `b' < b`.*
`Ordinal.mod_lt` theorem Ordinal.mod_lt : ∀ (a : Ordinal.{u_4}) {b : Ordinal.{u_4}}, b ≠ 0 → a % b < b The theorem `Ordinal.mod_lt` states that for any two ordinals `a` and `b` in the same type `u_4`, given that `b` is not zero, the modulus of `a` by `b` (denoted as `a % b`) is strictly less than `b`. In other words, it's the formalization of the familiar property from number theory that the remainder when one number is divided by another is always less than the divisor, but applied to ordinals. More concisely: For ordinals `a` and `b` in the same type with `b` non-zero, `a % b` strictly precedes `b`.
`Ordinal.lsub_le` theorem Ordinal.lsub_le : ∀ {ι : Type u_4} {f : ι → Ordinal.{max u_5 u_4}} {a : Ordinal.{max u_5 u_4}}, (∀ (i : ι), f i < a) → Ordinal.lsub f ≤ a This theorem states that for any type `ι` and any function `f` from `ι` to the type of ordinals, and any ordinal `a`, if every ordinal in the image of `f` is less than `a`, then the least strict upper bound of the ordinals obtained from `f` (which is denoted as `Ordinal.lsub f`) is less than or equal to `a`. Essentially, this theorem is saying if all elements of a set of ordinals are less than a given ordinal `a`, then the smallest ordinal that is larger than all elements of the set (if it exists) is also less than or equal to `a`. This is a formalization of a basic property of upper bounds in the setting of ordinals. More concisely: For any type `ι` and function `f` from `ι` to the type of ordinals, if every image `f(x)` is less than an ordinal `a`, then `Ordinal.lsup f` (the least upper bound of `f` if it exists) is less than or equal to `a`.
`Ordinal.div_zero` theorem Ordinal.div_zero : ∀ (a : Ordinal.{u_4}), a / 0 = 0 The theorem `Ordinal.div_zero` states that for any `Ordinal` `a`, the division of `a` by zero is zero. In other words, when any ordinal number is divided by zero, the result is always zero. This is a fundamental property of ordinal numbers in the context of division operations. More concisely: For any ordinal number `a`, `a / zero = zero`.
`Ordinal.limitRecOn.proof_4` theorem Ordinal.limitRecOn.proof_4 : ∀ (o : Ordinal.{u_1}), ¬o = 0 → (¬∃ a, o = Order.succ a) → o ≠ 0 ∧ ∀ a < o, Order.succ a < o The theorem `Ordinal.limitRecOn.proof_4` states that for any ordinal `o` that is not zero, and for which there does not exist an `a` such that `o` is the successor of `a`, it is true that `o` is not zero and for any `a` less than `o`, the successor of `a` is also less than `o`. This implies that `o` is a limit ordinal, i.e., an ordinal that is not zero and is not the successor of any ordinal, and hence, it also implies that limit ordinals are closed under taking successors. More concisely: For any non-zero limit ordinal `o`, for all `a` less than `o`, the successor of `a` is also less than `o`.
`Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.39` theorem Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.39 : ∀ (o : Ordinal.{u_3}), (0 ≤ o) = True This theorem states that for every ordinal 'o' in the type of well orders in a given type 'u_3', it is always true that 'o' is greater than or equal to zero. This is expressed in the theorem as `(0 ≤ o) = True`, which means that the inequality 'o is greater than or equal to zero' always holds for any ordinal 'o'. More concisely: Every ordinal in a given type is greater than or equal to zero. (or equivalently, the zero ordinal is less than or equal to every ordinal in the given type.)
`not_small_ordinal` theorem not_small_ordinal : ¬Small.{u, max (u + 1) (v + 1)} Ordinal.{max u v} This theorem states that the type of ordinals in universe `u` is not a small type of universe `u`. This theorem is a type-theoretic analogue of the Burali-Forti paradox, which states that there is no "set of all ordinals" because any set of ordinals has an ordinal associated with it, which leads to a contradiction. In the context of the Lean 4 type system, this translates to the claim that the type of all ordinals cannot be a small type, because small types are roughly analogous to sets. More concisely: The type of ordinals in a given universe is not a small type in that universe.
`Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.2` theorem Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.2 : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, (a = b) = (a ≤ b ∧ b ≤ a) This theorem from the Mathlib library in Lean 4 states that for any type `α` which has a partial order, two elements `a` and `b` of this type are equal if and only if `a` is less than or equal to `b` and `b` is less than or equal to `a`. In more mathematical terms, for all `α` with a partial order, `a = b` is equivalent to the statement `a ≤ b` and `b ≤ a`. This is a formal statement of the antisymmetry property in order theory. More concisely: In a partially ordered type `α`, elements `a` and `b` are equal if and only if they are mutually less than or equal to each other: `a = b <-> a ≤ b and b ≤ a`.
`Ordinal.sup_eq_bsup'` theorem Ordinal.sup_eq_bsup' : ∀ {o : Ordinal.{u}} {ι : Type u} (r : ι → ι → Prop) [inst : IsWellOrder ι r] (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}), Ordinal.sup (Ordinal.familyOfBFamily' r ho f) = o.bsup f The theorem `Ordinal.sup_eq_bsup'` states that for any ordinal `o` and any well-ordered type `ι`, given a relation `r` that provides a well-ordering for `ι`, and a function `f` that maps each ordinal less than `o` to another ordinal, the supremum of the family of ordinals as defined by applying `f` to the elements of `ι` (by converting `ι` to an ordinal using `r` and `ho = Ordinal.type r = o`) is equal to the supremum of ordinals obtained by applying `f` directly on ordinals less than `o`. In other words, this theorem shows the equality between two different ways of constructing a family of ordinals and then taking their supremum. More concisely: For any ordinal `o` and well-ordered type `ι` with relation `r`, if `f` maps ordinals less than `o` to ordinals, then `Ordinal.sup_eq_bsup' o r f` equals the supremum of `f` applied to ordinals less than `o`.
`Ordinal.mul_isNormal` theorem Ordinal.mul_isNormal : ∀ {a : Ordinal.{u_4}}, 0 < a → Ordinal.IsNormal fun x => a * x The theorem `Ordinal.mul_isNormal` states that for any ordinal `a` of the type `Ordinal`, if `a` is greater than zero, then the function that multiplies `a` with another ordinal `x` is a normal ordinal function. In other words, the function `f(x) = a * x` is strictly increasing and order-continuous. For a function to be order-continuous, the image of a limit ordinal under the function should be the supremum of the images of all ordinals less than the limit ordinal. More concisely: For any positive ordinal `a`, the function `x => a x` is a normal ordinal function. (Equivalently, it is strictly increasing and order-continuous.)*
`Ordinal.blsub_eq_lsub'` theorem Ordinal.blsub_eq_lsub' : ∀ {ι : Type u} (r : ι → ι → Prop) [inst : IsWellOrder ι r] (f : ι → Ordinal.{max u v}), (Ordinal.type r).blsub (Ordinal.bfamilyOfFamily' r f) = Ordinal.lsub f The theorem `Ordinal.blsub_eq_lsub'` states that for any type `ι`, any relation `r` on `ι` that forms a well-order, and any function `f` from `ι` to the set of ordinals, the least strict upper bound of the family of ordinals indexed by the set of ordinals less than the order type of `r` and converted to a family indexed by an ordinal using the specified well-ordering (`Ordinal.blsub (Ordinal.type r) (Ordinal.bfamilyOfFamily' r f)`) is equal to the least strict upper bound of the family of ordinals indexed directly by `ι` (`Ordinal.lsub f`). In simpler terms, it states that transforming the indexing set of a family of ordinals through a well-ordering doesn't change the least upper bound of that family. More concisely: For any type `ι`, well-order `r` on `ι`, and function `f : ι → Ordinal`, the least strict upper bound of the family `Ordinal.bfamilyOfFamily' r f` is equal to the least strict upper bound of the family `f`.
`Ordinal.zero_or_succ_or_limit` theorem Ordinal.zero_or_succ_or_limit : ∀ (o : Ordinal.{u_4}), o = 0 ∨ (∃ a, o = Order.succ a) ∨ o.IsLimit This theorem, `Ordinal.zero_or_succ_or_limit`, states that for any ordinal `o`, `o` is either zero, a successor of some element, or a limit ordinal. Specifically, an ordinal `o` is a successor of an element `a` if there exists such `a` that `o` equals to the successor of `a`. Meanwhile, an ordinal `o` is a limit ordinal if it is not zero and for all elements `a` less than `o`, the successor of `a` is still less than `o`. More concisely: Every ordinal is either zero, a successor of some ordinal, or a limit ordinal, where a limit ordinal is an ordinal greater than zero that is not the successor of any ordinal.
`Ordinal.omega_ne_zero` theorem Ordinal.omega_ne_zero : Ordinal.omega ≠ 0 This theorem asserts that the ordinal number `ω`, which is defined as the first infinite ordinal and corresponds to the order type of natural numbers, is not equal to zero. In other words, the infinite ordinal `ω` is distinct from the ordinal zero, emphasizing the non-finiteness of `ω`. More concisely: The theorem asserts that the infinite ordinal `ω` is not equal to zero.
`Ordinal.le_bsup` theorem Ordinal.le_bsup : ∀ {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}) (i : Ordinal.{u_4}) (h : i < o), f i h ≤ o.bsup f The theorem `Ordinal.le_bsup` states that for any ordinal `o`, for any function `f` that maps each ordinal less than `o` to another ordinal, and for any specific ordinal `i` which is less than `o`, the ordinal produced by applying the function `f` to `i` is less than or equal to the supremum of the family of ordinals generated by applying `f` to all ordinals less than `o`. This supremum is denoted by `Ordinal.bsup o f`. More concisely: For any ordinal `o` and function `f` mapping ordinals less than `o`, the image `f(i)` under `f` of each ordinal `i` less than `o` is less than or equal to the supremum `Ordinal.bsup o f` of all images under `f` of ordinals less than `o`.
`Ordinal.le_of_dvd` theorem Ordinal.le_of_dvd : ∀ {a b : Ordinal.{u_4}}, b ≠ 0 → a ∣ b → a ≤ b The theorem `Ordinal.le_of_dvd` states that for any two ordinals `a` and `b` of the same type, if `b` is not equal to zero and `a` divides `b`, then `a` is less than or equal to `b`. In mathematical terms, this theorem asserts that if we have a well-order `b` that is nonzero and another well-order `a` which divides `b`, then `a` cannot be strictly larger than `b`. More concisely: If `a` is an ordinal that divides a non-zero ordinal `b` of the same type, then `a` is less than or equal to `b`.
`Ordinal.enumOrd_def'_nonempty` theorem Ordinal.enumOrd_def'_nonempty : ∀ {S : Set Ordinal.{u}}, Set.Unbounded (fun x x_1 => x < x_1) S → ∀ (a : Ordinal.{u}), (S ∩ Set.Ici a).Nonempty The theorem `Ordinal.enumOrd_def'_nonempty` states that for any set `S` of ordinals, if `S` is unbounded (meaning that for every ordinal there is an element in `S` which is greater), then for any ordinal `a`, the intersection of `S` and the set of all ordinals greater than or equal to `a` (`Set.Ici a`) is non-empty. In other words, if a set of ordinals has no upper bound, then starting from any ordinal `a`, there are always elements from this set that are greater or equal to `a`. More concisely: If a set of ordinals is unbounded, then for any ordinal `a`, the set interesection of the set and the ordinals greater than or equal to `a` is non-empty.
`Ordinal.enumOrd_mem` theorem Ordinal.enumOrd_mem : ∀ {S : Set Ordinal.{u}}, Set.Unbounded (fun x x_1 => x < x_1) S → ∀ (o : Ordinal.{u}), Ordinal.enumOrd S o ∈ S := by sorry This theorem states that for any set `S` of ordinals (`Ordinal.{u}`), if `S` is unbounded (which means that for any ordinal `a`, there exists an ordinal `b` in `S` such that `b` is not less than `a`), then for any ordinal `o`, the ordinal `o` enumerated by the `Ordinal.enumOrd` function from the set `S` is an element of `S`. Essentially, it ensures that any ordinal obtained by enumerating from an unbounded set of ordinals is a member of that set. More concisely: If `S` is an unbounded set of ordinals, then for any ordinal `o`, `o` is in `S` if and only if `o` is enumerated by `Ordinal.enumOrd` from `S`.
`Ordinal.sub_le` theorem Ordinal.sub_le : ∀ {a b c : Ordinal.{u_4}}, a - b ≤ c ↔ a ≤ b + c This theorem, `Ordinal.sub_le`, states that for any three ordinals `a`, `b`, and `c`, the ordinal obtained by subtracting `b` from `a` is less than or equal to `c`, if and only if `a` is less than or equal to the sum of `b` and `c`. In mathematical notation, this can be stated as \(a - b \leq c \Leftrightarrow a \leq b + c\). This theorem establishes a connection between the operations of subtraction and addition on ordinals. More concisely: For any ordinals `a`, `b`, and `c`, `a - b <= c` if and only if `a <= b + c`.
`Ordinal.isNormal_iff_strictMono_limit` theorem Ordinal.isNormal_iff_strictMono_limit : ∀ (f : Ordinal.{u_4} → Ordinal.{u_5}), Ordinal.IsNormal f ↔ StrictMono f ∧ ∀ (o : Ordinal.{u_4}), o.IsLimit → ∀ (a : Ordinal.{u_5}), (∀ b < o, f b ≤ a) → f o ≤ a The theorem `Ordinal.isNormal_iff_strictMono_limit` states that for any function `f` mapping from an ordinal to another ordinal, `f` is a normal ordinal function if and only if `f` is strictly monotone (in other words, `f(a) < f(b)` whenever `a < b`), and furthermore if `o` is a limit ordinal, for any ordinal `a`, if all values `f(b)` for `b < o` are less than or equal to `a`, then `f(o)` must be less than or equal to `a`. This captures the defining property of a normal ordinal function: it is strictly increasing and its value at a limit ordinal is the least upper bound of its values at smaller ordinals. More concisely: A function between ordinals is normal if and only if it is strictly monotone and preserves limit ordinals' least upper bounds.
`Ordinal.lt_sup` theorem Ordinal.lt_sup : ∀ {ι : Type u} {f : ι → Ordinal.{max u v}} {a : Ordinal.{max u v}}, a < Ordinal.sup f ↔ ∃ i, a < f i The theorem `Ordinal.lt_sup` states that for any type `ι`, any function `f` from `ι` to `Ordinal` in the universe with maximum of `u` and `v`, and any ordinal `a` in the same universe, `a` is less than the supremum of `f` if and only if there exists an element `i` in `ι` such that `a` is less than `f(i)`. In other words, an ordinal is less than the supremum of a set of ordinals if and only if it is less than at least one ordinal in the set. More concisely: An ordinal `a` is less than the supremum of a function `f` from `ι` to `Ordinal` if and only if there exists an `i` in `ι` such that `a` is strictly less than `f(i)`.
`Ordinal.mod_one` theorem Ordinal.mod_one : ∀ (a : Ordinal.{u_4}), a % 1 = 0 The theorem `Ordinal.mod_one` states that for any well-ordered type `a` (represented as an ordinal in Lean), the result of calculating the modulus of `a` by 1 (`a % 1`) is always 0. This is essentially the ordinal version of the standard mathematical fact that any number modulo 1 is 0, reflecting the property that there is no remainder when any number is divided by 1. More concisely: For any well-ordered type `a` represented as an ordinal in Lean, `a % 1` equals 0.
`Ordinal.sub_self` theorem Ordinal.sub_self : ∀ (a : Ordinal.{u_4}), a - a = 0 The theorem `Ordinal.sub_self` states that for any ordinal `a`, subtracting `a` from itself results in zero. This is an instance of the property that in any number system, the subtraction of a number from itself yields zero. In the context of ordinals, which are equivalence classes of well-ordered sets, this theorem asserts that if we subtract an ordinal from itself, we obtain the ordinal zero, which represents the class of all empty well-ordered sets. More concisely: For any ordinal `a`, `a - a = 0`.
`Ordinal.sup_le_lsub` theorem Ordinal.sup_le_lsub : ∀ {ι : Type u} (f : ι → Ordinal.{max u v}), Ordinal.sup f ≤ Ordinal.lsub f This theorem states that for any indexed family of ordinals (represented as a function `f` from the index type `ι` to the type `Ordinal.{max u v}`), the supremum of that family (`Ordinal.sup f`) is less than or equal to the least strict upper bound of the family (`Ordinal.lsub f`). In other words, it ensures that the supremum of a set of ordinals is always less than or equal to the least ordinal that is greater than all the ordinals in the set. More concisely: The supremum of an indexed family of ordinals is less than or equal to their least upper bound.
`Ordinal.succ_lt_of_not_succ` theorem Ordinal.succ_lt_of_not_succ : ∀ {o b : Ordinal.{u_4}}, (¬∃ a, o = Order.succ a) → (Order.succ b < o ↔ b < o) This theorem states that for any two ordinals 'o' and 'b', if 'o' is not the successor of any ordinal ('o' is not of the form 'Order.succ a' for any 'a'), then the successor 'b' is less than 'o' if and only if 'b' is less than 'o'. In other words, if 'o' is not a successor ordinal, then whether 'b' is less than 'o' is the same as whether the successor of 'b' is less than 'o'. More concisely: For any ordinals 'o' and 'b', if 'o' is not a successor ordinal then 'b' < 'o' if and only if Order.succ 'b' < 'o'.
`Ordinal.bddAbove_range` theorem Ordinal.bddAbove_range : ∀ {ι : Type u} (f : ι → Ordinal.{max u v}), BddAbove (Set.range f) This theorem states that for any type `ι` and a function `f` that maps elements of `ι` to ordinals (well orders) living in a universe that is higher than the universe of `ι`, the set of all possible outputs of `f` (i.e., the range of `f`) is always bounded above. In other words, there always exists an ordinal that is greater than or equal to every ordinal in the output range of `f`. The theorem also refers to `Ordinal.lsub` for an explicit upper bound. More concisely: For any type `ι` and function `f` mapping elements of `ι` to ordinals living in a higher universe, the range of `f` is bounded above by some ordinal `α` such that `Ordinal.lsub α (f x)` for all `x` in `ι`.
`Ordinal.IsLimit.add` theorem Ordinal.IsLimit.add : ∀ (a : Ordinal.{u_4}) {b : Ordinal.{u_4}}, b.IsLimit → (a + b).IsLimit This theorem is an alias of `Ordinal.add_isLimit`. It states that for every ordinal `a` and for a limit ordinal `b`, the sum `a + b` is also a limit ordinal. Here, "ordinal" refers to a concept of order theory in mathematics, representing the class of well orders in a particular type, up to order isomorphism. A "limit ordinal" is a type of ordinal number that has no immediate predecessor. More concisely: For every ordinal `a` and limit ordinal `b`, the sum `a + b` is a limit ordinal.
`Ordinal.IsNormal.le_iff` theorem Ordinal.IsNormal.le_iff : ∀ {f : Ordinal.{u_4} → Ordinal.{u_5}}, Ordinal.IsNormal f → ∀ {a b : Ordinal.{u_4}}, f a ≤ f b ↔ a ≤ b This theorem states that for any normal ordinal function `f` mapping from an ordinal `a` to an ordinal `b`, `f(a)` is less than or equal to `f(b)` if and only if `a` is less than or equal to `b`. This essentially means that a normal ordinal function preserves the order of the ordinals. The normality of the function ensures its strict monotonicity and order-continuity. More concisely: A normal ordinal function preserves the order of ordinals: for all ordinals a and b, f(a) ≤ f(b) if and only if a ≤ b.
`Ordinal.one_add_omega` theorem Ordinal.one_add_omega : 1 + Ordinal.omega = Ordinal.omega The theorem `Ordinal.one_add_omega` states that if we add 1 to the first infinite ordinal, which we denote as `Ordinal.omega` and is defined as the order type of the natural numbers ℕ, the result is still `Ordinal.omega`. This captures the essence of infinity in ordinal arithmetic: adding a finite number (in this case 1) to an infinite ordinal does not change the infinite ordinal. More concisely: The first infinite ordinal `Ordinal.omega` equals the sum of itself and one, `Ordinal.omega + 1`.
`Ordinal.mul_add_div` theorem Ordinal.mul_add_div : ∀ (a : Ordinal.{u_4}) {b : Ordinal.{u_4}}, b ≠ 0 → ∀ (c : Ordinal.{u_4}), (b * a + c) / b = a + c / b This theorem states that for any ordinal number `a` and `c`, and any non-zero ordinal number `b`, the division of `b * a + c` by `b` is equal to `a + c / b`. This is essentially the division version of the distributive law for ordinal multiplication and addition. More concisely: For any ordinal numbers `a`, `b` (non-zero), and `c`, `(b a + c) / b = a + c / b`.*
`Ordinal.lsub_le_iff` theorem Ordinal.lsub_le_iff : ∀ {ι : Type u} {f : ι → Ordinal.{max u v}} {a : Ordinal.{max v u}}, Ordinal.lsub f ≤ a ↔ ∀ (i : ι), f i < a := by sorry The theorem `Ordinal.lsub_le_iff` states that for any type `ι`, any function `f` from `ι` to `Ordinal.{max u v}`, and any ordinal `a` of type `Ordinal.{max v u}`, the least strict upper bound of the family of ordinals defined by `f` is less than or equal to `a` if and only if every ordinal `f i` (where `i` is an element of `ι`) is less than `a`. In other words, `a` is an upper bound for all ordinals in the family defined by `f`, if and only if `a` is greater than every ordinal in that family. More concisely: For any type `ι`, function `f` from `ι` to the ordinals, and ordinal `a`, the least upper bound of the ordinals `f i` (where `i` is in `ι`) is less than or equal to `a` if and only if every `f i` is strictly less than `a`.
`Ordinal.mul_succ` theorem Ordinal.mul_succ : ∀ (a b : Ordinal.{u_4}), a * Order.succ b = a * b + a The theorem `Ordinal.mul_succ` states that for any two ordinal numbers `a` and `b`, the product of `a` and the successor of `b` (`Order.succ b`) is equal to the sum of the product of `a` and `b` with `a`. In mathematical terms, we say for all ordinals `a` and `b`, `a * (b + 1) = a * b + a`. This corresponds to the distribution law of multiplication over addition, specifically when adding one to a number (which is the definition of successor in this context). More concisely: For any ordinal numbers `a` and `b`, `a (Order.succ b) = a * b + a`.*
`Ordinal.omega_isLimit` theorem Ordinal.omega_isLimit : Ordinal.omega.IsLimit The theorem `Ordinal.omega_isLimit` states that the ordinal `ω` is a limit ordinal. In other words, the ordinal number `ω`, which is defined as the order type of the set of natural numbers, is not zero and is not the successor of any other ordinal. This implies that for all ordinals `a` less than `ω`, the successor of `a` is also less than `ω`. More concisely: The ordinal `ω` is a limit ordinal, meaning it is neither zero nor the successor of any ordinal.
`Ordinal.familyOfBFamily'.proof_1` theorem Ordinal.familyOfBFamily'.proof_1 : ∀ {ι : Type u_1} (r : ι → ι → Prop) [inst : IsWellOrder ι r] {o : Ordinal.{u_1}}, Ordinal.type r = o → ∀ (i : ι), Ordinal.typein r i < o This theorem asserts the following: for any type `ι`, any relation `r` on `ι` that gives it the structure of a well order, and any ordinal `o`, if the order type of `r` is equal to `o`, then the order type of every element `i` in `ι` (under the induced order `r`) is strictly less than `o`. This essentially implies that within a well-ordered set, the order type of each element is less than the order type of the entire set. More concisely: In a well-ordered set, the order type of each element is strictly less than the order type of the set.
`Ordinal.enumOrd_strictMono` theorem Ordinal.enumOrd_strictMono : ∀ {S : Set Ordinal.{u}}, Set.Unbounded (fun x x_1 => x < x_1) S → StrictMono (Ordinal.enumOrd S) The theorem `Ordinal.enumOrd_strictMono` states that for every set `S` of ordinals that is unbounded (in the sense that for every ordinal, there exists an ordinal in `S` that is larger), the function `Ordinal.enumOrd` that enumerates the ordinals in `S` is strictly monotone. In other words, if `a` is less than `b`, then the `a`th ordinal in `S` is less than the `b`th ordinal in `S`. This is expressed in mathematical notation as: for all `a` and `b`, `a < b` implies `Ordinal.enumOrd(S)(a) < Ordinal.enumOrd(S)(b)`. More concisely: For every unbounded set `S` of ordinals, the function `Ordinal.enumOrd(S)` is a strictly increasing enumeration of `S`.
`Ordinal.lt_omega` theorem Ordinal.lt_omega : ∀ {o : Ordinal.{u_1}}, o < Ordinal.omega ↔ ∃ n, o = ↑n The theorem `Ordinal.lt_omega` states that for all ordinals 'o', 'o' is less than the first infinite ordinal (denoted as 'ω' in Lean 4) if and only if there exists a natural number 'n' such that 'o' is equal to the ordinal representation of 'n'. Here, the first infinite ordinal 'ω' is defined as the order type of the set of natural numbers. More concisely: For every ordinal 'o', 'o' is strictly less than the first infinite ordinal 'ω' if and only if there exists a natural number 'n' such that 'o' is the ordinal representation of 'n'.
`Ordinal.IsLimit.pos` theorem Ordinal.IsLimit.pos : ∀ {o : Ordinal.{u_4}}, o.IsLimit → 0 < o The theorem `Ordinal.IsLimit.pos` states that for any ordinal `o`, if `o` is a limit ordinal, then `o` is greater than zero. In other words, it asserts that all limit ordinals are positive. More concisely: For every limit ordinal `o`, `o` is a positive ordinal.
`Ordinal.mul_lt_mul_iff_left` theorem Ordinal.mul_lt_mul_iff_left : ∀ {a b c : Ordinal.{u_4}}, 0 < a → (a * b < a * c ↔ b < c) The theorem `Ordinal.mul_lt_mul_iff_left` states that for any three ordinals `a`, `b` and `c` (in the same universe), if `a` is greater than zero, then the product of `a` and `b` is less than the product of `a` and `c` if and only if `b` is less than `c`. This theorem is an analogue of a similar property in the domain of real numbers, expressing an interaction between multiplication and order in the context of ordinals. More concisely: For any ordinals `a > 0`, `b`, and `c`, `a b < a * c` if and only if `b < c`.*
`Ordinal.enumOrd_def_nonempty` theorem Ordinal.enumOrd_def_nonempty : ∀ {S : Set Ordinal.{u}}, Set.Unbounded (fun x x_1 => x < x_1) S → ∀ {o : Ordinal.{u}}, {x \| x ∈ S ∧ ∀ c < o, Ordinal.enumOrd S c < x}.Nonempty The theorem `Ordinal.enumOrd_def_nonempty` states that for any set `S` of ordinals and any ordinal `o`, if `S` is unbounded by the relation `x < x_1`, then there exists an element `x` in `S` such that for every `c` less than `o`, the ordinal enumerated by `S` and `c` is less than `x`. In other words, if `S` is a set of ordinals that is unbounded in the sense that for any ordinal we can always find a larger one in `S`, then for any given ordinal, we can find an ordinal in `S` larger than all ordinals we can enumerate from `S` that are less than the given ordinal. More concisely: If `S` is an unbounded set of ordinals, then for every ordinal `o`, there exists an ordinal `x` in `S` such that for all ordinals `c` less than `o`, the ordinal enumerated by `S` and `c` is less than `x`.
`WellFounded.rank_lt_of_rel` theorem WellFounded.rank_lt_of_rel : ∀ {α : Type u} {r : α → α → Prop} {a b : α} (hwf : WellFounded r), r a b → hwf.rank a < hwf.rank b The theorem `WellFounded.rank_lt_of_rel` states that for any type `α` and any well-founded relation `r` on `α`, if `a` and `b` are elements of `α` where the relation `r a b` holds (meaning `a` is related to `b` by `r`), then the rank of `a` under the relation `r` is less than the rank of `b`. This is to say, in a well-founded relation, any element has a rank that is strictly less than the rank of any element it is related to. More concisely: In a well-founded relation on a type `α`, if `a` is related to `b` (`r a b` holds), then the rank of `a` is strictly less than the rank of `b`.
`Ordinal.div_nonempty` theorem Ordinal.div_nonempty : ∀ {a b : Ordinal.{u_4}}, b ≠ 0 → {o \| a < b * Order.succ o}.Nonempty The theorem `Ordinal.div_nonempty` states that for any two ordinals `a` and `b`, if `b` is not equal to zero, then there exists at least one ordinal `o` such that `a` is less than the product of `b` and the successor of `o`. This theorem is about the non-emptiness of the set in the definition of ordinal division. More concisely: For any non-zero ordinals `a` and `b`, there exists an ordinal `o` such that `a` is strictly less than `b (o + 1)`.*
`Ordinal.bsup_le` theorem Ordinal.bsup_le : ∀ {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v}} {a : Ordinal.{max u v}}, (∀ (i : Ordinal.{u}) (h : i < o), f i h ≤ a) → o.bsup f ≤ a The theorem `Ordinal.bsup_le` states that for any ordinal `o`, function `f` from a smaller ordinal to another ordinal, and ordinal `a`, if for all `i` less than `o`, `f(i)` is less than or equal to `a`, then the supremum of the family of ordinals indexed by the ordinals less than `o` (computed by `Ordinal.bsup o f`) is also less than or equal to `a`. In other words, if all ordinals in a family are bounded above by `a`, then the least upper bound (supremum) of the family, obtained by `Ordinal.bsup`, is also bounded above by `a`. More concisely: For any ordinal `o`, function `f` from a smaller ordinal to an ordinal, and ordinal `a`, if `f(i) ≤ a` for all `i` less than `o`, then `Ordinal.bsup o f ≤ a`.
`Ordinal.add_sub_cancel` theorem Ordinal.add_sub_cancel : ∀ (a b : Ordinal.{u_4}), a + b - a = b In natural language, the theorem `Ordinal.add_sub_cancel` can be described as follows: For any two ordinals `a` and `b`, the theorem states that if you add `a` and `b` together, and then subtract `a` from the result, you will be left with `b`. In other words, the operation of adding `a` to `b` and then subtracting `a` from the sum results in a no-op for `a`, essentially "cancelling" it out and leaving `b` unchanged. This property holds for all ordinals and is a fundamental property related to ordinal arithmetic. More concisely: For all ordinals `a` and `b`, `a + b = b + a`.
`Ordinal.lsub_not_mem_range` theorem Ordinal.lsub_not_mem_range : ∀ {ι : Type u} (f : ι → Ordinal.{max u v}), Ordinal.lsub f ∉ Set.range f := by sorry This theorem states that for any type `ι` and any function `f` from `ι` to the type of well orders, the least strict upper bound of the family of ordinals defined by `f` does not belong to the range of `f`. In mathematical terms, if we consider `f` as a function that assigns to each element of `ι` an ordinal number, then the least strict upper bound of all these ordinal numbers is not an image of any element in `ι` under the function `f`. More concisely: The least strict upper bound of a family of ordinals, each being the image of some element under a given function from a type to the type of ordinals, is not an image under that function.
`Ordinal.mex_not_mem_range` theorem Ordinal.mex_not_mem_range : ∀ {ι : Type u} (f : ι → Ordinal.{max u v}), Ordinal.mex f ∉ Set.range f This theorem states that for any type `ι` and any function `f` mapping `ι` to an ordinal, the minimum excluded ordinal of the function `f` is not in the range of `f`. In other words, there is no element in `ι` such that when it is mapped by `f`, it gives the minimum ordinal that `f` fails to attain. This is akin to saying that the smallest ordinal number that is not produced by the function `f` cannot be produced by `f`, a statement about the "gaps" in the ordinal numbers produced by the function `f`. More concisely: For any type `ι` and function `f` from `ι` to an ordinal, the minimum excluded ordinal of `f` is not in the image of `f`.
`Ordinal.omega_pos` theorem Ordinal.omega_pos : 0 < Ordinal.omega The theorem `Ordinal.omega_pos` states that zero is less than `Ordinal.omega`, or in other words, the first infinite ordinal, typically known as ω. Recall that `Ordinal.omega` is defined as the order type of the set of natural numbers ℕ. Therefore, this theorem essentially asserts that the order type of the natural numbers, an infinite set, is strictly greater than zero. More concisely: The theorem `Ordinal.omega_pos` asserts that 0 < ω, where ω is the order type of the natural numbers.
`Ordinal.sub_nonempty` theorem Ordinal.sub_nonempty : ∀ {a b : Ordinal.{u_4}}, {o \| a ≤ b + o}.Nonempty This theorem states that for any two ordinals `a` and `b` in `Type u_4`, there exists at least one ordinal `o` such that `a` is less than or equal to the sum of `b` and `o`. In other words, the set of all ordinals `o` that satisfy the inequality `a ≤ b + o` is nonempty. More concisely: For any ordinals `a` and `b`, there exists an ordinal `o` such that `a <= b + o`.
`Ordinal.mul_lt_mul_of_pos_left` theorem Ordinal.mul_lt_mul_of_pos_left : ∀ {a b c : Ordinal.{u_4}}, a < b → 0 < c → c * a < c * b The theorem `Ordinal.mul_lt_mul_of_pos_left` states that for any three ordinal numbers `a`, `b`, and `c` from the same type, if `a` is less than `b` and `c` is greater than zero, then the product of `c` and `a` is less than the product of `c` and `b`. In other words, multiplying a smaller ordinal number by a positive ordinal number results in a smaller ordinal than when multiplying the larger ordinal number by the same positive ordinal number. More concisely: For all ordinal numbers `a`, `b`, and `c` of the same type, if `a` < `b` and `c` > 0, then `c a` < `c * b`.*
`Ordinal.sup_eq_lsub_iff_succ` theorem Ordinal.sup_eq_lsub_iff_succ : ∀ {ι : Type u} (f : ι → Ordinal.{max u v}), Ordinal.sup f = Ordinal.lsub f ↔ ∀ a < Ordinal.lsub f, Order.succ a < Ordinal.lsub f This theorem states that for a given function `f` mapping the type `ι` to ordinals, the supremum of `f` equals the least strict upper bound of `f` if and only if for any ordinal `a` that is less than the least strict upper bound of `f`, the successor of `a` is also less than the least strict upper bound of `f`. In simpler terms, this theorem is essentially asserting a relationship between the supremum and least upper bound of a set of ordinals: they are equivalent if and only if every element less than the least upper bound has its successor also less than the least upper bound. More concisely: The supremum of a function from a type to ordinals equals the least strict upper bound if and only if the successor of every ordinal strictly below it is also strictly below the least upper bound.
`Ordinal.le_add_sub` theorem Ordinal.le_add_sub : ∀ (a b : Ordinal.{u_4}), a ≤ b + (a - b) This theorem, `Ordinal.le_add_sub`, states that for any two ordinals `a` and `b`, the ordinal `a` is less than or equal to the sum of ordinal `b` and the difference between `a` and `b`. This is a fundamental property of ordinals, similar to the property in real numbers that any number is less than or equal to the sum of another number and the difference between the first number and the second one. More concisely: For all ordinals `a` and `b`, `a ≤ b + (a - b)`.
`Ordinal.div_lt` theorem Ordinal.div_lt : ∀ {a b c : Ordinal.{u_4}}, b ≠ 0 → (a / b < c ↔ a < b * c) This theorem states that for any three ordinals `a`, `b`, and `c`, given that `b` is not equal to zero, the ordinal `a` divided by `b` is less than `c` if and only if `a` is less than the product of `b` and `c`. This establishes a relationship between ordinal division and multiplication, similar to the property in number theory that for positive numbers `a`, `b` and `c`, `a` divided by `b` is less than `c` if and only if `a` is less than `b` times `c`. More concisely: For any ordinals `a`, `b` with `b ≠ 0`, `a / b < c` if and only if `a < b c`.*
`Ordinal.sup_le` theorem Ordinal.sup_le : ∀ {ι : Type u} {f : ι → Ordinal.{max u v}} {a : Ordinal.{max u v}}, (∀ (i : ι), f i ≤ a) → Ordinal.sup f ≤ a := by sorry The theorem `Ordinal.sup_le` states that for any type `ι`, any function `f` mapping from `ι` to the order type `Ordinal.{max u v}`, and any ordinal `a`, if every ordinal in the range of `f` is less than or equal to `a`, then the supremum of the set of ordinals generated by `f` is also less than or equal to `a`. In other words, if every ordinal that `f` can produce is bounded above by `a`, then the largest such ordinal (the supremum) is also bounded above by `a`. More concisely: If `f` is a function from an ordinal `ι` to the ordinals such that the image of `f` is bounded above by an ordinal `a`, then the supremum of the image of `f` is also less than or equal to `a`.
`Ordinal.sub_zero` theorem Ordinal.sub_zero : ∀ (a : Ordinal.{u_4}), a - 0 = a The theorem `Ordinal.sub_zero` states that for any ordinal 'a', subtracting zero from 'a' is equal to 'a' itself. In other words, this theorem is saying that if you take any well-ordered type 'a' and subtract 0 from it, you will always get 'a' back. This is a reflection of the general arithmetic property that anything minus zero equals itself, but applied specifically to the type of well-ordered types, or "ordinals", in Lean 4. More concisely: For any ordinal 'a', 'a' - 0 = a.
`Ordinal.IsNormal.lt_iff` theorem Ordinal.IsNormal.lt_iff : ∀ {f : Ordinal.{u_4} → Ordinal.{u_5}}, Ordinal.IsNormal f → ∀ {a b : Ordinal.{u_4}}, f a < f b ↔ a < b This theorem states that for any normal ordinal function `f`, and any two ordinals `a` and `b`, `f(a)` is less than `f(b)` if and only if `a` is less than `b`. In other words, a normal ordinal function `f` preserves the order of ordinals: if an ordinal `a` is less than another ordinal `b`, then `f(a)` is also less than `f(b)` and vice versa. More concisely: For any normal ordinal function `f`, if `a` is less than `b`, then `f(a)` is less than `f(b)`.
`Ordinal.bsup_le_iff` theorem Ordinal.bsup_le_iff : ∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {a : Ordinal.{max u v}}, o.bsup f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h ≤ a The theorem `Ordinal.bsup_le_iff` states that for any ordinal `o`, any function `f` that maps each ordinal less than `o` to an ordinal, and any ordinal `a`, the supremum of the family of ordinals generated by `f` is less than or equal to `a` if and only if for every ordinal `i` less than `o`, `f(i)` is less than or equal to `a`. In other words, the supremum is less than or equal to `a` precisely when all elements of the family are less than or equal to `a`. More concisely: For any ordinal `o`, function `f` mapping ordinals less than `o` to ordinals, and ordinal `a`, if `f(i) ≤ a` for all `i` less than `o`, then the supremum of the family generated by `f` is less than or equal to `a`.
`Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.44` theorem Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.44 : ∀ {α : Sort u_1} {p : α → Prop}, (¬∀ (x : α), p x) = ∃ x, ¬p x This theorem states that, for any type `α` and any property `p` applicable to `α`, the statement "it is not the case that for all `x` of type `α`, `p` applies to `x`" is equivalent to "there exists an `x` of type `α` such that `p` does not apply to `x`". In other words, the negation of universal quantification (not all `x` have property `p`) is equivalent to the existence of an object that does not have the property (there exists an `x` such that `x` does not have property `p`). More concisely: The negation of "forall x : α, p(x)" is equivalent to "exists x : α, ¬p(x)".
`Ordinal.le_sup` theorem Ordinal.le_sup : ∀ {ι : Type u} (f : ι → Ordinal.{max u v}) (i : ι), f i ≤ Ordinal.sup f The theorem `Ordinal.le_sup` states that for any type `ι` and any function `f` from `ι` to the type of well-ordered sets `Ordinal`, each element `f i` (where `i` is in `ι`) is less than or equal to the supremum of the set of well-ordered sets generated by `f`. In other words, any ordinal in the family defined by `f` is less than or equal to the supremum of the family of ordinals. More concisely: For any type `ι` and function `f` from `ι` to the well-ordered sets `Ordinal`, `f i ≤ sup (map f ι)` for all `i` in `ι`.
`Ordinal.pred_eq_iff_not_succ` theorem Ordinal.pred_eq_iff_not_succ : ∀ {o : Ordinal.{u_4}}, o.pred = o ↔ ¬∃ a, o = Order.succ a The theorem `Ordinal.pred_eq_iff_not_succ` states that for any ordinal `o`, the predecessor of `o` is equal to `o` if and only if there doesn't exist an ordinal `a` such that `o` is the successor of `a`. In other words, an ordinal is equal to its predecessor precisely when it's not the successor of any other ordinal. More concisely: For any ordinal `o`, `o = pred o` if and only if there is no ordinal `a` such that `o = succ a`.
`Ordinal.sub_le_self` theorem Ordinal.sub_le_self : ∀ (a b : Ordinal.{u_4}), a - b ≤ a The theorem `Ordinal.sub_le_self` asserts that for any two ordinals `a` and `b` in any universe `u_4`, the difference of `a` and `b` (denoted as `a - b`) is less than or equal to `a`. In other words, subtracting any ordinal `b` from an ordinal `a` will always result in an ordinal that is less than or equal to `a`. This is a formalization of the common mathematical property that for any two numbers, the difference between them is always less than or equal to the original number, adapted for the context of ordinal numbers. More concisely: For all ordinals `a` and `b`, `a - b` is less than or equal to `a`.
`Ordinal.lt_sub` theorem Ordinal.lt_sub : ∀ {a b c : Ordinal.{u_4}}, a < b - c ↔ c + a < b The theorem `Ordinal.lt_sub` states that for any three ordinals `a`, `b`, and `c`, the inequality `a` is less than `b - c` holds if and only if `c + a` is less than `b`. In simple terms, it establishes an equivalence between two forms of inequality involving ordinal numbers. More concisely: For any ordinals `a`, `b`, and `c`, `a` < `b` if and only if `c + a` < `b`.
`Ordinal.bsup_le_blsub` theorem Ordinal.bsup_le_blsub : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}), o.bsup f ≤ o.blsub f This theorem, `Ordinal.bsup_le_blsub`, states that for any ordinal `o` and any function `f` that maps each ordinal less than `o` to another ordinal, the supremum (`bsup`) of the family of all such ordinals generated by `f` is less than or equal to the least strict upper bound (`blsub`) of the same family. In other words, the highest ordinal that can be reached by `f` for all ordinals less than `o` is always less than or equal to the smallest ordinal that is strictly greater than all ordinals in the same family. More concisely: For any ordinal `o` and function `f` mapping ordinals below `o`, the supremum of the image of `f` is less than or equal to the least strict upper bound of the domain of `f`.
`Ordinal.limitRecOn.proof_2` theorem Ordinal.limitRecOn.proof_2 : ∀ {C : Ordinal.{u_2} → Sort u_1} (o : Ordinal.{u_2}), (∃ a, o = Order.succ a) → C o = C (Order.succ o.pred) := by sorry This theorem says that for all ordinals `o` and for any function `C` from ordinals to any type, if `o` is the successor of some ordinal, then the value of `C` at `o` is equal to the value of `C` at the successor of the predecessor of `o`. In other words, given a function `C` defined on ordinals and an ordinal `o` that is a successor, we can replace `o` with the successor of its predecessor in the function `C` without changing the value of `C(o)`. More concisely: For any function `C` from ordinals to a type and for all successor ordinals `o`, `C(o) = C(suc (pred o))`, where `suc` and `pred` denote the successor and predecessor functions on ordinals, respectively.
`Ordinal.lt_blsub` theorem Ordinal.lt_blsub : ∀ {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}) (i : Ordinal.{u_4}) (h : i < o), f i h < o.blsub f This theorem, `Ordinal.lt_blsub`, states that for any ordinal `o`, any function `f` that maps each ordinal less than `o` to another ordinal, and any ordinal `i` that is strictly less than `o`, the value of `f` at `i` is strictly less than the least strict upper bound of the family of ordinals indexed by the set of ordinals less than `o`. In mathematical terms, for all ordinals `o` and `i` with `i < o`, and for all functions `f: {a in Ordinals \| a < o} -> Ordinals`, we have `f(i) < blsub(o, f)`. More concisely: For every ordinal `o` and `i` with `i < o`, and for any function `f` mapping ordinals less than `o` to ordinals, we have `f(i) < sup i.in (f)`. Here, `sup` denotes the least upper bound or the supremum. The notation `i.in (f)` is used to denote the set of ordinals less than `o` as the domain of function `f`.
`Ordinal.limitRecOn_succ` theorem Ordinal.limitRecOn_succ : ∀ {C : Ordinal.{u_4} → Sort u_5} (o : Ordinal.{u_4}) (H₁ : C 0) (H₂ : (o : Ordinal.{u_4}) → C o → C (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → o.IsLimit → ((o' : Ordinal.{u_4}) → o' < o → C o') → C o), (Order.succ o).limitRecOn H₁ H₂ H₃ = H₂ o (o.limitRecOn H₁ H₂ H₃) The theorem `Ordinal.limitRecOn_succ` states that for any type constructor `C` mapping an ordinal to a type, any ordinal `o`, and three hypotheses, the limit recursion on the successor of `o` is equivalent to the application of the second hypothesis on `o` and the limit recursion on `o`. The three hypotheses are: `H₁` which is a type `C` for the ordinal `0`, `H₂` which maps an ordinal `o` and a type `C o` to another type `C (Order.succ o)`, and `H₃` which applies to a limit ordinal `o` and a function that maps any ordinal smaller than `o` to a type `C o'`. Limit recursion is a method to define a value or function on all ordinals by specifying its value at `0`, at successors, and at limit ordinals. More concisely: For any type constructor `C` and ordinal `o`, the limit recursion on `succ(o)` using hypotheses `H₁`, `H₂`, and `H₃` is equivalent to applying `H₂` on `o` and `C o` and then using `H₃` on `o` and the limit recursion on `o`.
`Ordinal.mul_div_le` theorem Ordinal.mul_div_le : ∀ (a b : Ordinal.{u_4}), b * (a / b) ≤ a The theorem `Ordinal.mul_div_le` states that for any two ordinals `a` and `b`, the product of `b` and the quotient of `a` divided by `b` is less than or equal to `a`. In other words, it's asserting that if you divide an ordinal `a` by another ordinal `b`, and then multiply the result by `b`, you get a value that is no greater than the original ordinal `a`. This is a form of the mathematical property that division and multiplication are inverse operations. More concisely: For all ordinals a and b, a ÷ b b ≤ a.*
`Ordinal.IsNormal.eq_iff_zero_and_succ` theorem Ordinal.IsNormal.eq_iff_zero_and_succ : ∀ {f g : Ordinal.{u} → Ordinal.{u}}, Ordinal.IsNormal f → Ordinal.IsNormal g → (f = g ↔ f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (Order.succ a) = g (Order.succ a)) This theorem states that for any two normal ordinal functions `f` and `g`, `f` is equal to `g` if and only if `f` and `g` map the ordinal zero to the same ordinal and for all ordinals `a`, if `f` and `g` map `a` to the same ordinal, then `f` and `g` also map the successor of `a` to the same ordinal. Here, a normal ordinal function is a strictly increasing function which is order-continuous, meaning the image of a limit ordinal is the supremum of the function values for all smaller ordinals. The successor of an ordinal is the next ordinal if it exists, or the same ordinal if it is maximal. More concisely: Two normal ordinal functions are equal if and only if they map ordinal zero to the same ordinal and agree on all successor ordinals.
`Ordinal.sup_eq_bsup` theorem Ordinal.sup_eq_bsup : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}), Ordinal.sup (o.familyOfBFamily f) = o.bsup f The theorem `Ordinal.sup_eq_bsup` states that for any ordinal `o` and any function `f` from ordinals less than `o` to ordinals, the supremum of the family of ordinals obtained by applying `f` to the elements of the well-ordered set corresponding to `o` (obtained via `Ordinal.familyOfBFamily`) is equal to the supremum of the family of ordinals indexed by the set of ordinals less than `o` (obtained via `Ordinal.bsup`). In other words, the result of applying the supremum operation to the family of ordinals indexed by a well-ordered set is the same as applying the supremum operation to the family of ordinals indexed by the ordinals less than a given ordinal. This shows an equivalence between two ways of computing a supremum over a family of ordinals. More concisely: For any ordinal `o` and function `f` from ordinals less than `o` to ordinals, the supremum of `Ordinal.familyOfBFamily o f` equals `Ordinal.bsup (range o) (map f (range (O < o)))`.
`Ordinal.IsNormal.isLimit` theorem Ordinal.IsNormal.isLimit : ∀ {f : Ordinal.{u_4} → Ordinal.{u_5}}, Ordinal.IsNormal f → ∀ {o : Ordinal.{u_4}}, o.IsLimit → (f o).IsLimit := by sorry The theorem `Ordinal.IsNormal.isLimit` states that for any normal ordinal function `f` and for any ordinal `o` which is a limit ordinal, the image of `o` under `f`, denoted by `f o`, is also a limit ordinal. In other words, if `f` is a normal ordinal function (i.e., it is strictly increasing and order-continuous), and `o` is a limit ordinal (i.e., it is not zero and not a successor ordinal), then the ordinal `f o` is also a limit ordinal. More concisely: If `f` is a normal ordinal function and `o` is a limit ordinal, then `f o` is also a limit ordinal.
`Ordinal.IsNormal.self_le` theorem Ordinal.IsNormal.self_le : ∀ {f : Ordinal.{u_4} → Ordinal.{u_4}}, Ordinal.IsNormal f → ∀ (a : Ordinal.{u_4}), a ≤ f a The theorem `Ordinal.IsNormal.self_le` states that for any normal function `f` mapping ordinals to ordinals, any ordinal `a` is less than or equal to `f(a)`. In other words, a normal ordinal function always produces an output that is greater than or equal to its input. This is a property of normal functions in the context of ordinal numbers. More concisely: For any normal function `f` mapping ordinals to ordinals, `a ≤ f(a)` for all ordinals `a`.
`Ordinal.limit_le` theorem Ordinal.limit_le : ∀ {o : Ordinal.{u_4}}, o.IsLimit → ∀ {a : Ordinal.{u_4}}, o ≤ a ↔ ∀ x < o, x ≤ a The theorem `Ordinal.limit_le` states that for every ordinal `o` which is a limit ordinal, and another ordinal `a`, the ordinal `o` is less than or equal to `a` if and only if all ordinals `x` that are less than `o` are also less than or equal to `a`. This means that, in the set of ordinals, a limit ordinal is less than or equal to another ordinal if every ordinal smaller than the limit ordinal is also less than or equal to that other ordinal. More concisely: A limit ordinal is less than or equal to another ordinal if and only if every ordinal less than the limit ordinal is less than or equal to that other ordinal.
`Ordinal.div_add_mod` theorem Ordinal.div_add_mod : ∀ (a b : Ordinal.{u_4}), b * (a / b) + a % b = a The theorem `Ordinal.div_add_mod` states that for any two ordinals `a` and `b`, the product of `b` and the quotient of `a` divided by `b`, when added to the remainder of `a` divided by `b`, equals `a`. This is an analogue to the division theorem in the context of ordinals, which are types of well orders, and reflects the property that any natural number can be represented uniquely as the product of two numbers plus a remainder. More concisely: For any ordinals `a` and `b`, `(a : adversal) ÷ b (a % b) = a`, where `÷` and `%` denote ordinal division and remainder, respectively.*
`Ordinal.limitRecOn.proof_1` theorem Ordinal.limitRecOn.proof_1 : ∀ {C : Ordinal.{u_2} → Sort u_1} (o : Ordinal.{u_2}), o = 0 → C o = C 0 The theorem `Ordinal.limitRecOn.proof_1` states that for any function `C` from ordinals in `Type u_2` to the type `Sort u_1` and any ordinal `o` from `Type u_2`, if `o` is equal to the ordinal 0, then the value of `C` at `o` is the same as the value of `C` at 0. This theorem essentially states that, under the provided conditions, the function `C` behaves the same way at `o` and at 0. More concisely: For any function `C` from ordinals to a type and any ordinal `o`, if `o` equals 0, then `C o` equals `C 0`.
`Ordinal.lsub_unique` theorem Ordinal.lsub_unique : ∀ {ι : Type u_4} [inst : Unique ι] (f : ι → Ordinal.{max u_5 u_4}), Ordinal.lsub f = Order.succ (f default) := by sorry The theorem `Ordinal.lsub_unique` states that for any type `ι` which has a unique instance, and any function `f` that maps `ι` to an Ordinal of type `Ordinal.{max u_5 u_4}`, the least strict upper bound of the family of ordinals defined by `f` is equal to the successor of the value of `f` at the default instance of `ι`. In mathematical terms, if we have a unique element from a type `ι` and a function `f` mapping this element to an ordinal, the least strict upper bound of the set of ordinals generated by `f` is just the successor of the ordinal `f` maps the unique element to. More concisely: If `ι` has a unique instance and `f : ι → Ordinal` is a function, then the least upper bound of the image of `f` is the successor of `(f! default)`, where `default` is the default instance of `ι`.
`Ordinal.bddAbove_iff_small` theorem Ordinal.bddAbove_iff_small : ∀ {s : Set Ordinal.{u}}, BddAbove s ↔ Small.{u, u + 1} ↑s The theorem `Ordinal.bddAbove_iff_small` establishes an equivalence between two conditions for a set of ordinals, which is a type representing well orders. Specifically, it states that for any set `s` of ordinals, `s` is bounded above (i.e., there exists an ordinal that is greater than or equal to every ordinal in `s`) if and only if `s` is "small". Here, "small" is a type-theoretic property that means the elements of the set `s` can be indexed by some ordinal, i.e., there exists a surjective function from an ordinal to `s`. More concisely: A set of ordinals is bounded above if and only if it is "small," meaning it can be indexed by some ordinal.
`Ordinal.div_le` theorem Ordinal.div_le : ∀ {a b c : Ordinal.{u_4}}, b ≠ 0 → (a / b ≤ c ↔ a < b * Order.succ c) This theorem, `Ordinal.div_le`, states that for any three ordinals `a`, `b`, and `c`, as long as `b` is not zero, the proposition that `a` divided by `b` is less than or equal to `c` is equivalent to the proposition that `a` is strictly less than the product of `b` and the successor of `c`. The successor of an ordinal is the next greater ordinal, except when the ordinal is maximal, in which case its successor is itself. More concisely: For ordinals `a`, `b` with `b ≠ 0`, `a / b ≤ c` is equivalent to `a < b (c + 1)`.*
`Ordinal.blsub_le_iff` theorem Ordinal.blsub_le_iff : ∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {a : Ordinal.{max u v}}, o.blsub f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h < a This theorem, `Ordinal.blsub_le_iff`, states that for any ordinal `o`, function `f` from ordinals less than `o` to ordinals, and ordinal `a`, the least strict upper bound of the family of ordinals indexed by the set of ordinals less than `o` (denoted as `Ordinal.blsub o f`) is less than or equal to `a` if and only if, for all ordinals `i` that are less than `o`, `f(i)` is less than `a`. In other words, it provides a characterization of the least upper bound in terms of the ordinals less than the index `o`. More concisely: For any ordinal `o`, function `f` from ordinals less than `o` to ordinals, and ordinal `a`, `Ordinal.blsub o f` is less than or equal to `a` if and only if `f(i)` is less than `a` for all `i` less than `o`.
`Ordinal.IsNormal.bsup_eq` theorem Ordinal.IsNormal.bsup_eq : ∀ {f : Ordinal.{u} → Ordinal.{max u v}}, Ordinal.IsNormal f → ∀ {o : Ordinal.{u}}, o.IsLimit → (o.bsup fun x x_1 => f x) = f o This theorem states that for all normal ordinal functions `f` and for every limit ordinal `o`, the supremum of the family of ordinals indexed by the set of ordinals less than `o` (where each element is given by the function `f`) is equal to `f o`. In other words, if a function `f` is normal and `o` is a limit ordinal, then the supremum of the function values for ordinals less than `o` equals the function value at `o`. This theorem is an important result related to the behavior of strictly increasing and order-continuous functions on limit ordinals. More concisely: For every normal function `f` and limit ordinal `o`, `f o` is the supremum of the values `{f x \| x < o}` in the ordered structure of ordinals.
`Ordinal.add_sub_cancel_of_le` theorem Ordinal.add_sub_cancel_of_le : ∀ {a b : Ordinal.{u_4}}, b ≤ a → b + (a - b) = a The theorem `Ordinal.add_sub_cancel_of_le` states that for any two ordinals `a` and `b` in the same type universe `u_4`, if `b` is less than or equal to `a`, then adding `b` to the difference of `a` and `b` results in `a`. In other words, if `b ≤ a`, then `b + (a - b) = a`. This is similar to the cancellation law of addition in ordinal arithmetic. More concisely: For any ordinals `a` and `b` in the same type universe, if `b ≤ a`, then `a = a + (b - b)`.
`Ordinal.enumOrd_def'` theorem Ordinal.enumOrd_def' : ∀ {S : Set Ordinal.{u}} (o : Ordinal.{u}), Ordinal.enumOrd S o = sInf (S ∩ Set.Ici (o.blsub fun a x => Ordinal.enumOrd S a)) The theorem `Ordinal.enumOrd_def'` provides a characteristic equation for the function `Ordinal.enumOrd`, which enumerates unbounded sets of ordinals. For any set of ordinals `S` and an ordinal `o`, the value of `Ordinal.enumOrd S o` is equal to the greatest lower bound (`sInf`) of the intersection (`∩`) between `S` and the set of all ordinals that are greater than or equal to (`Set.Ici`) the ordinal obtained by applying the function `o.blsub fun a x => Ordinal.enumOrd S a`. This theorem, however, might not be the easiest to work with, hence `enumOrd_def` is suggested for use instead. More concisely: The theorem `Ordinal.enumOrd_def` states that for any set of ordinals `S` and ordinal `o`, `Ordinal.enumOrd S o` is the greatest lower bound of `S ∩ Set.Ici (o.map (Ordinal.enumOrd S))`.
`Ordinal.add_le_of_limit` theorem Ordinal.add_le_of_limit : ∀ {a b c : Ordinal.{u_4}}, b.IsLimit → (a + b ≤ c ↔ ∀ b' < b, a + b' ≤ c) The theorem `Ordinal.add_le_of_limit` states that for any three ordinals `a`, `b`, and `c` where `b` is a limit ordinal (i.e., not zero and not a successor), the sum of `a` and `b` is less than or equal to `c` if and only if for all `b'` less than `b`, the sum of `a` and `b'` is less than or equal to `c`. It essentially expresses a property about addition of ordinals in relation to limit ordinals. More concisely: For any limit ordinal `b` and ordinals `a` and `c`, `a + b <= c` if and only if `a + b' <= c` for all `b' < b`.
`Ordinal.enumOrd_def` theorem Ordinal.enumOrd_def : ∀ {S : Set Ordinal.{u}} (o : Ordinal.{u}), Ordinal.enumOrd S o = sInf (S ∩ {b \| ∀ c < o, Ordinal.enumOrd S c < b}) The theorem `Ordinal.enumOrd_def` provides a more practical definition for the function `Ordinal.enumOrd`. For any set `S` of ordinals and any ordinal `o`, it states that the enumerator function `Ordinal.enumOrd` applied to `S` and `o` is equal to the infimum (or greatest lower bound) of the intersection of `S` and the set of all ordinals `b` such that for all ordinals `c` less than `o`, `Ordinal.enumOrd S c` is less than `b`. This means `Ordinal.enumOrd` picks out the lowest ordinal in `S` that's greater than all the previously enumerated ordinals. More concisely: The theorem `Ordinal.enumOrd_def` asserts that for any set `S` of ordinals and any ordinal `o`, `Ordinal.enumOrd S o` is the greatest ordinal `b` in `S` that is greater than every `Ordinal.enumOrd S c` for `c < o`.
`Ordinal.limitRecOn.proof_3` theorem Ordinal.limitRecOn.proof_3 : ∀ (o : Ordinal.{u_1}), (∃ a, o = Order.succ a) → o.pred < o The theorem `Ordinal.limitRecOn.proof_3` states that for any ordinal `o`, if there exists another ordinal `a` such that `o` is the successor of `a` (i.e., `o = Order.succ a`), then the predecessor of `o` (as determined by the function `Ordinal.pred`) is strictly less than `o`. In essence, if `o` is a successor ordinal, then its predecessor is a lesser ordinal. More concisely: For any ordinal `o` and `a`, if `o` is the successor of `a` (`o = Order.succ a`), then `Ordinal.pred o < o`.
`Ordinal.add_isLimit` theorem Ordinal.add_isLimit : ∀ (a : Ordinal.{u_4}) {b : Ordinal.{u_4}}, b.IsLimit → (a + b).IsLimit The theorem `Ordinal.add_isLimit` states that for any ordinal `a` and any ordinal `b` that is a limit ordinal, the sum of `a` and `b` is also a limit ordinal. In other words, if `b` is an ordinal such that it is not zero and not a successor, then the ordinal resulting from the addition of `a` and `b` also shares these properties. More concisely: If `a` is an ordinal and `b` is a limit ordinal, then `a + b` is a limit ordinal.
`Ordinal.limitRecOn_limit` theorem Ordinal.limitRecOn_limit : ∀ {C : Ordinal.{u_4} → Sort u_5} (o : Ordinal.{u_4}) (H₁ : C 0) (H₂ : (o : Ordinal.{u_4}) → C o → C (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → o.IsLimit → ((o' : Ordinal.{u_4}) → o' < o → C o') → C o) (h : o.IsLimit), o.limitRecOn H₁ H₂ H₃ = H₃ o h fun x _h => x.limitRecOn H₁ H₂ H₃ The theorem `Ordinal.limitRecOn_limit` states that for any type C indexed by ordinals, any ordinal `o`, and any functions `H₁`, `H₂`, and `H₃` defined appropriately, if `o` is a limit ordinal, then performing the limit ordinal recursion on `o` using `H₁`, `H₂`, and `H₃` is the same as applying `H₃` to `o`, the fact that `o` is a limit ordinal, and the recursion on all ordinals less than `o`. In other words, this theorem guarantees the correctness of the limit case for a general recursive definition on ordinals, stating that when the recursion reaches a limit ordinal, it behaves as expected; it applies the limit case function `H₃` to the current ordinal and the results of the recursion on all smaller ordinals. More concisely: For any type indexed by ordinals, if a limit ordinal `o` and functions `H₁`, `H₂`, and `H₃` are given, then limit recursion on `o` using `H₁`, `H₂`, and `H₃` equals `H₃(o)` concatenated with the results of recursively applying `H₃` to all ordinals less than `o`.
`Ordinal.limitRecOn_zero` theorem Ordinal.limitRecOn_zero : ∀ {C : Ordinal.{u_4} → Sort u_5} (H₁ : C 0) (H₂ : (o : Ordinal.{u_4}) → C o → C (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → o.IsLimit → ((o' : Ordinal.{u_4}) → o' < o → C o') → C o), Ordinal.limitRecOn 0 H₁ H₂ H₃ = H₁ The theorem `Ordinal.limitRecOn_zero` states that for any type family `C` indexed over ordinals, given that `C` holds for the ordinal `0`, `C` holds for the successor of any ordinal `o` given that `C` holds for `o`, and `C` holds for any limit ordinal `o` given that `C` holds for all ordinals less than `o`, then the limit recursion on `0` with these properties is equal to the given proof that `C` holds for `0`. In other words, the theorem provides the base case for a form of ordinal recursion, stating that the recursion at zero is just the initial element `H₁`. More concisely: Given a type family `C` indexed over ordinals satisfying `C 0`, `C (o + 1)` for all `o`, and `C o` for limit ordinals `o`, the limit recursion on `0` of `C` is equal to the proof that `C 0` holds.
`Ordinal.one_lt_omega` theorem Ordinal.one_lt_omega : 1 < Ordinal.omega This theorem states that the ordinal number one is less than omega. In other words, the ordinal corresponding to the number one is smaller than the first infinite ordinal, denoted as omega. Omega is defined as the order type of the set of natural numbers, which means it corresponds to the concept of "countable infinity" in set theory. More concisely: One is a strictly smaller ordinal than omega.
`Ordinal.add_isNormal` theorem Ordinal.add_isNormal : ∀ (a : Ordinal.{u_4}), Ordinal.IsNormal fun x => a + x The theorem `Ordinal.add_isNormal` states that for any ordinal `a`, the function that adds `a` to its input is a normal ordinal function. In other words, this function is strictly increasing and order-continuous. In mathematical terms, for any two ordinals `x` and `y`, if `x < y`, then `a + x < a + y`. Moreover, if `o` is a limit ordinal, then `a + o` is the supremum of `a + b` for all `b < o`. More concisely: For any ordinal `a`, the function `x => a + x: Ordinal → Ordinal` is both strictly increasing and order-continuous.
`Ordinal.IsNormal.sup` theorem Ordinal.IsNormal.sup : ∀ {f : Ordinal.{max u v} → Ordinal.{max u w}}, Ordinal.IsNormal f → ∀ {ι : Type u} (g : ι → Ordinal.{max u v}) [inst : Nonempty ι], f (Ordinal.sup g) = Ordinal.sup (f ∘ g) This theorem states that for any normal ordinal function `f`, the function `f` applied to the supremum of a family of ordinals `g` (assuming that the family of ordinals is nonempty) equals the supremum of the function `f` applied to each ordinal in the family `g`. Here, a normal ordinal function is defined as a strictly increasing function that also satisfies the property of order-continuity. In other words, if `f` is a normal ordinal function and `g` is a family of ordinals, then the supremum of the image of `g` under `f` is the same as the image under `f` of the supremum of `g`. More concisely: For any normal ordinal function `f` and nonempty family `g` of ordinals, `f( sup g) = sup (f ∘ g)`.
`Ordinal.lift_succ` theorem Ordinal.lift_succ : ∀ (a : Ordinal.{v}), Ordinal.lift.{u, v} (Order.succ a) = Order.succ (Ordinal.lift.{u, v} a) This theorem states that for any ordinal `a` in a certain universe `v`, lifting the successor of `a` to a larger universe (which universe is at least the maximum of `u` and `v`), is the same as first lifting `a` to the larger universe and then taking its successor. In other words, the operation of taking the successor commutes with the operation of lifting ordinals to a larger universe. More concisely: For any ordinal `a` and universes `u` and `v` with `v` at least `u`, the lift of the successor of `a` in `v` equals the successor of the lift of `a` in `v`.
`Ordinal.bsup_eq_sup'` theorem Ordinal.bsup_eq_sup' : ∀ {ι : Type u} (r : ι → ι → Prop) [inst : IsWellOrder ι r] (f : ι → Ordinal.{max u v}), (Ordinal.type r).bsup (Ordinal.bfamilyOfFamily' r f) = Ordinal.sup f The theorem `Ordinal.bsup_eq_sup'` states that for every type `ι`, every relation `r` on `ι` constituting a well-order, and every function `f` from `ι` to the type of ordinals, the supremum of the family of ordinals indexed by the set of ordinals less than the ordinal type of `r` (computed using `Ordinal.bsup` and `Ordinal.bfamilyOfFamily' r f`) is equal to the supremum of the family of ordinals produced by `f` (computed using `Ordinal.sup f`). In simpler terms, it says that the supremum of a family of ordinals doesn't change when we change the indexing set from a given type to the ordinals less than the ordinal type of a well-ordering on that type. More concisely: For every well-ordered type `ι`, every relation `r` on `ι`, and every monotonic function `f` from `ι` to the ordinals, the supremum of `Ordinal.bsup (Ordinal.bfamilyOfFamily' r f)` equals `Ordinal.sup f`.
`Ordinal.pred_succ` theorem Ordinal.pred_succ : ∀ (o : Ordinal.{u_4}), (Order.succ o).pred = o The theorem `Ordinal.pred_succ` states that for any ordinal `o`, when you take the successor of `o` and then its predecessor, you get `o` back. In other words, the predecessor function undoes the effect of the successor function on the set of ordinals. This can be thought of as a property of ordinal arithmetic much like the property in basic number theory where subtracting 1 from a number that was just incremented by 1 returns the original number. More concisely: For any ordinal number `o`, the predecessor of the successor of `o` equals `o`: `∀ (o : Ordinal), pred (pred (o.successor)) = o`.
`Cardinal.ord_aleph0` theorem Cardinal.ord_aleph0 : Cardinal.aleph0.ord = Ordinal.omega This theorem states that the ordinal corresponding to the smallest infinite cardinal (`ℵ₀`) is the first infinite ordinal (`ω`). In other words, when we map the smallest infinite cardinal to an ordinal using the `Cardinal.ord` function, we obtain the first infinite ordinal. This relationship holds true within the mathematical framework of ordinal and cardinal numbers, where `ℵ₀` corresponds to the cardinality of the set of natural numbers and `ω` is the order type of the natural numbers. More concisely: The smallest infinite cardinal `ℵ₀` maps to the first infinite ordinal `ω` under the `Cardinal.ord` function.
`Ordinal.lsub_eq_blsub` theorem Ordinal.lsub_eq_blsub : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}), Ordinal.lsub (o.familyOfBFamily f) = o.blsub f This theorem states that for any ordinal `o` and a function `f` mapping each ordinal less than `o` to an ordinal, the least strict upper bound of the family of ordinals (mapped by `f` and indexed by the set of ordinals less than `o`) obtained through the function `Ordinal.familyOfBFamily` is equal to the least strict upper bound of the same family of ordinals directly obtained through `f` using the function `Ordinal.blsub`. In other words, the operations `Ordinal.lsub` and `Ordinal.blsub` yield the same result when applied to the same set of ordinals under the conditions mentioned. More concisely: For any ordinal `o` and function `f` mapping ordinals less than `o` to ordinals, `Ordinal.lsub (Ordinal.familyOfBFamily o f) = Ordinal.blsub (∑ (x : Ordinal) in set.Ico 0 o) (λ (x : Ordinal), f x)`.
`Ordinal.add_left_cancel` theorem Ordinal.add_left_cancel : ∀ (a : Ordinal.{u_4}) {b c : Ordinal.{u_4}}, a + b = a + c ↔ b = c The theorem `Ordinal.add_left_cancel` states that for any ordinal number `a` and for any two other ordinal numbers `b` and `c` in the same type, if the sum of `a` and `b` equals the sum of `a` and `c`, then `b` equals `c`. This theorem is basically asserting the property of left-cancellation in ordinal addition. In mathematical terms, if a + b = a + c, then b = c for any ordinals a, b, and c. More concisely: If for ordinal numbers `a`, `b`, and `c`, `a + b = a + c`, then `b = c`.
`Ordinal.lsub_empty` theorem Ordinal.lsub_empty : ∀ {ι : Type u_4} [h : IsEmpty ι] (f : ι → Ordinal.{max u_5 u_4}), Ordinal.lsub f = 0 := by sorry The theorem `Ordinal.lsub_empty` states that for any type `ι` that is empty (i.e., it has no elements), and any function `f` from `ι` to the ordinals (of type `Ordinal.{max u_5 u_4}`), the least strict upper bound of the family of ordinals defined by `f` (denoted as `Ordinal.lsub f`) is zero. In other words, if you have an empty set of ordinals, the smallest ordinal that is strictly greater than all ordinals in the set is zero. More concisely: If `ι` is empty, then the least upper bound of the ordinal family `f : ι → Ordinal` is zero.
`Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.18` theorem Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.18 : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, (¬a < b) = (b ≤ a) This theorem from the Mathlib library in Set Theory's Ordinal Arithmetic section states that for any given type `α` with a linear order, for any two elements `a` and `b` of this type, the condition of `a` not being less than `b` (`¬a < b`) is equivalent to `b` being less than or equal to `a` (`b ≤ a`). This is a basic property of ordered sets being formalized, and mirrors the statement we have in mathematics that if one element is not smaller than another, then the second must be smaller or equal to the first. More concisely: For any linear order type `α`, the conditions `a ≤ b` and `¬a < b` are equivalent for all elements `a` and `b` of `α`.
`Ordinal.le_div` theorem Ordinal.le_div : ∀ {a b c : Ordinal.{u_4}}, c ≠ 0 → (a ≤ b / c ↔ c * a ≤ b) This theorem, `Ordinal.le_div`, states that for any three ordinals `a`, `b`, and `c` in a certain type, if `c` is not zero, then `a` is less than or equal to the quotient of `b` by `c` if and only if `c` multiplied by `a` is less than or equal to `b`. In other words, it establishes an equivalence between the "divided" comparison (`a ≤ b / c`) and the "multiplied" comparison (`c * a ≤ b`) within the context of ordinal numbers, provided that the divisor `c` is non-zero. More concisely: For ordinal numbers `a`, `b`, and `c` (with `c` non-zero), `a ≤ b / c` if and only if `c a ≤ b`.*
`Ordinal.IsNormal.trans` theorem Ordinal.IsNormal.trans : ∀ {f : Ordinal.{u_4} → Ordinal.{u_5}} {g : Ordinal.{u_6} → Ordinal.{u_4}}, Ordinal.IsNormal f → Ordinal.IsNormal g → Ordinal.IsNormal (f ∘ g) The theorem `Ordinal.IsNormal.trans` states that for any two ordinal-valued functions `f` and `g`, if both `f` and `g` are normal, then their composition `(f ∘ g)` is also normal. Here, a normal function is defined as a strictly increasing function which is order-continuous. That is, for a limit ordinal `o`, its image under the function is the supremum of the images of the ordinals less than `o`. More concisely: If `f` and `g` are normal ordinal-valued functions, then their composition `(f ∘ g)` is also a normal ordinal-valued function.
`Ordinal.blsub_le` theorem Ordinal.blsub_le : ∀ {o : Ordinal.{u_4}} {f : (b : Ordinal.{u_4}) → b < o → Ordinal.{max u_4 u_5}} {a : Ordinal.{max u_4 u_5}}, (∀ (i : Ordinal.{u_4}) (h : i < o), f i h < a) → o.blsub f ≤ a The theorem `Ordinal.blsub_le` states that for any ordinal `o`, function `f` from ordinals less than `o` to ordinals, and any ordinal `a`, if for all `i` less than `o`, `f(i)` is less than `a`, then the least strict upper bound of the family of ordinals defined by `f` and indexed by the set of ordinals less than `o` is less than or equal to `a`. More concisely: If `f` is a function from ordinals less than `o` to ordinals such that `f(i)` is less than `a` for all `i` less than `o`, then the least upper bound of the family `{f(i) \| i < o}` is less than or equal to `a`.
`Ordinal.IsNormal.le_iff_eq` theorem Ordinal.IsNormal.le_iff_eq : ∀ {f : Ordinal.{u_4} → Ordinal.{u_4}}, Ordinal.IsNormal f → ∀ {a : Ordinal.{u_4}}, f a ≤ a ↔ f a = a The theorem `Ordinal.IsNormal.le_iff_eq` states that for all ordinal functions `f` that are normal, and for any ordinal `a`, the function value `f(a)` is less than or equal to `a` if and only if `f(a)` equals `a`. This means that in the context of normal ordinal functions, the only way for `f(a)` to be less than or equal to `a` is for `f(a)` to be exactly equal to `a`. More concisely: For any normal ordinal function `f` and ordinal `a`, `f(a) ≤ a` if and only if `f(a) = a`.
`Ordinal.lt_lsub` theorem Ordinal.lt_lsub : ∀ {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) (i : ι), f i < Ordinal.lsub f The theorem `Ordinal.lt_lsub` states that, for any type `ι` and a function `f` from `ι` to the type of well orders `Ordinal` (up to order isomorphism), any value `f i` for a particular `i` in `ι` is less than the least strict upper bound of the family of ordinals defined by `f`. In other words, for any given ordinal in the family, the least strict upper bound of the entire family is always greater. More concisely: For any type `ι` and function `f` from `ι` to `Ordinal`, `f i` is strictly less than the least upper bound of the family `{f x \| x ∈ ι}`.
`Ordinal.IsNormal.monotone` theorem Ordinal.IsNormal.monotone : ∀ {f : Ordinal.{u_4} → Ordinal.{u_5}}, Ordinal.IsNormal f → Monotone f The theorem `Ordinal.IsNormal.monotone` states that for any function `f` from an ordinal to another ordinal, if `f` is a normal ordinal function, then `f` is monotone. In other words, if `f` is strictly increasing and order-continuous (the image of a limit ordinal is the supremum of the images of ordinals less than it), then `f` preserves the order, i.e., if `a` is less than or equal to `b`, then `f(a)` is less than or equal to `f(b)`. More concisely: If `f` is a normal function from an ordinal to another ordinal, then `f` is monotone.
`Ordinal.div_one` theorem Ordinal.div_one : ∀ (a : Ordinal.{u_4}), a / 1 = a This theorem states that for any ordinal number `a`, the quotient of `a` divided by one is `a` itself. In terms of ordinal arithmetic, this is equivalent to saying that division by one has no effect on an ordinal number. More concisely: For any ordinal number `a`, `a / 1 = a`.
`Ordinal.IsNormal.limit_le` theorem Ordinal.IsNormal.limit_le : ∀ {f : Ordinal.{u_4} → Ordinal.{u_5}}, Ordinal.IsNormal f → ∀ {o : Ordinal.{u_4}}, o.IsLimit → ∀ {a : Ordinal.{u_5}}, f o ≤ a ↔ ∀ b < o, f b ≤ a This theorem states that for any normal ordinal function `f` and any limit ordinal `o`, the value of `f` at `o` is less than or equal to an ordinal `a` if and only if for all ordinals `b` less than `o`, `f(b)` is less than or equal to `a`. In other words, the value of a normal ordinal function at a limit ordinal is the least upper bound of its values at smaller ordinals. More concisely: For any normal ordinal function `f` and limit ordinal `o`, `f(o)` is the least upper bound of `{f(x) \| x < o}` if and only if `f(o)` is less than or equal to `a` for all ordinals `a` less than `o`.
`Ordinal.nat_lt_omega` theorem Ordinal.nat_lt_omega : ∀ (n : ℕ), ↑n < Ordinal.omega The theorem `Ordinal.nat_lt_omega` states that for any natural number `n`, the ordinal representation of `n` is less than the first infinite ordinal, `Ordinal.omega`. In other words, every natural number is less than the cardinality of the set of all natural numbers, represented as an ordinal. This reflects the intuitive understanding that any specific natural number is part of a set that is infinitely large. More concisely: For any natural number `n`, the ordinal representation of `n` is strictly less than the ordinal `Ordinal.omega`.
`Ordinal.mul_div_cancel` theorem Ordinal.mul_div_cancel : ∀ (a : Ordinal.{u_4}) {b : Ordinal.{u_4}}, b ≠ 0 → b * a / b = a The theorem `Ordinal.mul_div_cancel` states that for any ordinal 'a' and any non-zero ordinal 'b', the result of multiplying 'b' and 'a' and then dividing by 'b' is equal to 'a'. In other words, in the context of ordinal arithmetic, multiplication and division by a non-zero ordinal 'b' are inverse operations. More concisely: For any non-zero ordinal b, the multiplication and division operations are inverse on ordinals, i.e., a b / b = a for all ordinals a.*
`Acc.rank_lt_of_rel` theorem Acc.rank_lt_of_rel : ∀ {α : Type u} {r : α → α → Prop} {a b : α} (hb : Acc r b) (h : r a b), ⋯.rank < hb.rank This theorem states that for any two elements `a` and `b` of a type `α`, given a relation `r` between elements of `α`, if `r a b` holds true and `b` is accessible (Acc) under the relation `r`, then the rank of `a` is strictly less than the rank of `b`. The concept of rank used here refers to an ordinal associated with each element under the given relation, often used in the context of well-foundedness. More concisely: If `a` and `b` are elements of type `α`, `r` is a relation on `α` with `r a b` and `b` accessible under `r`, then the rank of `a` is strictly less than the rank of `b` under `r`.
`Ordinal.range_familyOfBFamily` theorem Ordinal.range_familyOfBFamily : ∀ {α : Type u_1} {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → α), Set.range (o.familyOfBFamily f) = o.brange f The theorem `Ordinal.range_familyOfBFamily` claims that for any type `α`, any ordinal `o`, and any function `f` which takes an ordinal `a` and a proof that `a` is less than `o` to `α`, the set of all values that `f` can take (i.e., the image of `f`, denoted as `Set.range (Ordinal.familyOfBFamily o f)`) is equal to the set of all values that `f` can take when indexed over the ordinals less than `o` (denoted as `Ordinal.brange o f`). In simpler terms, regardless of whether the function is indexed over all ordinals or just those less than a given ordinal, the set of its possible outputs remains the same. More concisely: For any type α, ordinal o, and function f from ordinals to α with proof of each index being less than o, the sets {f a : a < o} and {f b : ∃ i, i < o ∧ b = i} are equal.
`Ordinal.eq_enumOrd` theorem Ordinal.eq_enumOrd : ∀ {S : Set Ordinal.{u}} (f : Ordinal.{u} → Ordinal.{u}), Set.Unbounded (fun x x_1 => x < x_1) S → (StrictMono f ∧ Set.range f = S ↔ f = Ordinal.enumOrd S) The theorem `Ordinal.eq_enumOrd` characterizes the function `enumOrd` in the context of set theory. For any set `S` of ordinals and any function `f` from ordinals to ordinals, if `S` is an unbounded set (where "unbounded" means that for any ordinal, there exists an ordinal in `S` that is not smaller), then `f` is strictly monotonic (i.e., if `a` is less than `b`, then `f(a)` is less than `f(b)`) and the range of `f` equals `S` if and only if `f` is equivalent to the function `enumOrd` applied on `S`. In other words, `enumOrd` is the unique strictly monotonic function whose range is the unbounded set `S` of ordinals. More concisely: For any unbounded set S of ordinals, the function f is equal to enumOrd on S if and only if f is a strict monotonic function with range S.
`Ordinal.mex_le_of_ne` theorem Ordinal.mex_le_of_ne : ∀ {ι : Type u_4} {f : ι → Ordinal.{max u_5 u_4}} {a : Ordinal.{max u_5 u_4}}, (∀ (i : ι), f i ≠ a) → Ordinal.mex f ≤ a The theorem `Ordinal.mex_le_of_ne` states that for any type `ι`, any function `f` mapping from `ι` to Ordinals, and any ordinal `a`, if `a` is not equal to `f(i)` for all `i` in `ι`, then the minimum excluded ordinal in the family of ordinals given by `f` is less than or equal to `a`. In other words, if `a` is an ordinal that is not in the range of `f`, then `a` is greater than or equal to the smallest ordinal that is also not in the range of `f`. More concisely: For any type `ι`, function `f` from `ι` to Ordinals, and ordinal `a`, if `a` is not in the image of `f`, then there exists an ordinal `x` in the image of `f` such that `x < a`.
`Ordinal.IsNormal.strictMono` theorem Ordinal.IsNormal.strictMono : ∀ {f : Ordinal.{u_4} → Ordinal.{u_5}}, Ordinal.IsNormal f → StrictMono f := by sorry This theorem states that for any function `f` from ordinals to ordinals, if `f` is a normal ordinal function, then `f` is also strictly monotone. In other words, if `f` is a function which is strictly increasing and the image of a limit ordinal under `f` is the supremum of the images of all smaller ordinals, then for any two ordinals `a` and `b`, if `a` is less than `b`, `f(a)` is less than `f(b)`. More concisely: If `f` is a normal ordinal function, then it is strictly increasing.
`Ordinal.lsub_typein` theorem Ordinal.lsub_typein : ∀ (o : Ordinal.{u}), Ordinal.lsub (Ordinal.typein fun x x_1 => x < x_1) = o The theorem `Ordinal.lsub_typein` states that for any ordinal `o`, the least strict upper bound (lsub) of the order type function (i.e., `Ordinal.typein`) applied to the less-than relation over its elements is equal to `o` itself. This essentially means that the least upper bound of the order types of all elements, when considered within a well-order, is the ordinal representing the well-order itself. More concisely: For any ordinal `o`, the least upper bound of the order types of elements in `o` is equal to `o`.
`Ordinal.sup_le_iff` theorem Ordinal.sup_le_iff : ∀ {ι : Type u} {f : ι → Ordinal.{max u v}} {a : Ordinal.{max u v}}, Ordinal.sup f ≤ a ↔ ∀ (i : ι), f i ≤ a := by sorry The theorem `Ordinal.sup_le_iff` states that for any type `ι`, any function `f` from `ι` to the type of ordinals, and any ordinal `a`, the supremum of the family of ordinals given by `f` is less than or equal to `a` if and only if every ordinal `f i` for `i` in `ι` is less than or equal to `a`. In other words, the supremum of a set of ordinals is less than or equal to an ordinal `a` if and only if all ordinals in the set are less than or equal to `a`. More concisely: The supremum of a family of ordinals \(f(i)\), where \(f\) is a function from a type \(\ι\) to the type of ordinals, is less than or equal to an ordinal \(a\) if and only if every \(f(i)\) is less than or equal to \(a\) for all \(i\) in \(\ι\).
`Ordinal.lt_mul_succ_div` theorem Ordinal.lt_mul_succ_div : ∀ (a : Ordinal.{u_4}) {b : Ordinal.{u_4}}, b ≠ 0 → a < b * Order.succ (a / b) := by sorry This theorem states that for any ordinal 'a' and any non-zero ordinal 'b', 'a' is less than the product of 'b' and the successor of the quotient of 'a' by 'b'. In mathematical terms, for all a, b ∈ Ordinal, with b ≠ 0, we have a < b * succ(a / b). Here, 'succ' denotes the successor function, which gives the next ordinal after the input ordinal. More concisely: For any ordinal a and non-zero ordinal b, a is strictly below the product of b and the successor of the quotient of a by b. (a < b (succ (a / b)))*

LeanAide GPT-4 documentation

Module: Mathlib.SetTheory.Ordinal.Arithmetic

Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.10

theorem Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.10 : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, (¬a ≤ b) = (b < a)

Ordinal.enumOrd_surjective

theorem Ordinal.enumOrd_surjective : ∀ {S : Set Ordinal.{u}}, Set.Unbounded (fun x x_1 => x < x_1) S → ∀ s ∈ S, ∃ a, Ordinal.enumOrd S a = s

Ordinal.mul_le_of_limit

theorem Ordinal.mul_le_of_limit : ∀ {a b c : Ordinal.{u_4}}, b.IsLimit → (a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c)

Ordinal.mod_lt

theorem Ordinal.mod_lt : ∀ (a : Ordinal.{u_4}) {b : Ordinal.{u_4}}, b ≠ 0 → a % b < b

Ordinal.lsub_le

theorem Ordinal.lsub_le : ∀ {ι : Type u_4} {f : ι → Ordinal.{max u_5 u_4}} {a : Ordinal.{max u_5 u_4}}, (∀ (i : ι), f i < a) → Ordinal.lsub f ≤ a

Ordinal.div_zero

theorem Ordinal.div_zero : ∀ (a : Ordinal.{u_4}), a / 0 = 0

Ordinal.limitRecOn.proof_4

theorem Ordinal.limitRecOn.proof_4 : ∀ (o : Ordinal.{u_1}), ¬o = 0 → (¬∃ a, o = Order.succ a) → o ≠ 0 ∧ ∀ a < o, Order.succ a < o

Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.39

theorem Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.39 : ∀ (o : Ordinal.{u_3}), (0 ≤ o) = True

not_small_ordinal

theorem not_small_ordinal : ¬Small.{u, max (u + 1) (v + 1)} Ordinal.{max u v}

Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.2

theorem Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.2 : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, (a = b) = (a ≤ b ∧ b ≤ a)

Ordinal.sup_eq_bsup'

theorem Ordinal.sup_eq_bsup' : ∀ {o : Ordinal.{u}} {ι : Type u} (r : ι → ι → Prop) [inst : IsWellOrder ι r] (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}), Ordinal.sup (Ordinal.familyOfBFamily' r ho f) = o.bsup f

Ordinal.mul_isNormal

theorem Ordinal.mul_isNormal : ∀ {a : Ordinal.{u_4}}, 0 < a → Ordinal.IsNormal fun x => a * x

Ordinal.blsub_eq_lsub'

theorem Ordinal.blsub_eq_lsub' : ∀ {ι : Type u} (r : ι → ι → Prop) [inst : IsWellOrder ι r] (f : ι → Ordinal.{max u v}), (Ordinal.type r).blsub (Ordinal.bfamilyOfFamily' r f) = Ordinal.lsub f

Ordinal.zero_or_succ_or_limit

theorem Ordinal.zero_or_succ_or_limit : ∀ (o : Ordinal.{u_4}), o = 0 ∨ (∃ a, o = Order.succ a) ∨ o.IsLimit

Ordinal.omega_ne_zero

theorem Ordinal.omega_ne_zero : Ordinal.omega ≠ 0

Ordinal.le_bsup

theorem Ordinal.le_bsup : ∀ {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}) (i : Ordinal.{u_4}) (h : i < o), f i h ≤ o.bsup f

Ordinal.le_of_dvd

theorem Ordinal.le_of_dvd : ∀ {a b : Ordinal.{u_4}}, b ≠ 0 → a ∣ b → a ≤ b

Ordinal.enumOrd_def'_nonempty

theorem Ordinal.enumOrd_def'_nonempty : ∀ {S : Set Ordinal.{u}}, Set.Unbounded (fun x x_1 => x < x_1) S → ∀ (a : Ordinal.{u}), (S ∩ Set.Ici a).Nonempty

Ordinal.enumOrd_mem

theorem Ordinal.enumOrd_mem : ∀ {S : Set Ordinal.{u}}, Set.Unbounded (fun x x_1 => x < x_1) S → ∀ (o : Ordinal.{u}), Ordinal.enumOrd S o ∈ S := by sorry

Ordinal.sub_le

theorem Ordinal.sub_le : ∀ {a b c : Ordinal.{u_4}}, a - b ≤ c ↔ a ≤ b + c

Ordinal.isNormal_iff_strictMono_limit

theorem Ordinal.isNormal_iff_strictMono_limit : ∀ (f : Ordinal.{u_4} → Ordinal.{u_5}), Ordinal.IsNormal f ↔ StrictMono f ∧ ∀ (o : Ordinal.{u_4}), o.IsLimit → ∀ (a : Ordinal.{u_5}), (∀ b < o, f b ≤ a) → f o ≤ a

Ordinal.lt_sup

theorem Ordinal.lt_sup : ∀ {ι : Type u} {f : ι → Ordinal.{max u v}} {a : Ordinal.{max u v}}, a < Ordinal.sup f ↔ ∃ i, a < f i

Ordinal.mod_one

theorem Ordinal.mod_one : ∀ (a : Ordinal.{u_4}), a % 1 = 0

Ordinal.sub_self

theorem Ordinal.sub_self : ∀ (a : Ordinal.{u_4}), a - a = 0

Ordinal.sup_le_lsub

theorem Ordinal.sup_le_lsub : ∀ {ι : Type u} (f : ι → Ordinal.{max u v}), Ordinal.sup f ≤ Ordinal.lsub f

Ordinal.succ_lt_of_not_succ

theorem Ordinal.succ_lt_of_not_succ : ∀ {o b : Ordinal.{u_4}}, (¬∃ a, o = Order.succ a) → (Order.succ b < o ↔ b < o)

Ordinal.bddAbove_range

theorem Ordinal.bddAbove_range : ∀ {ι : Type u} (f : ι → Ordinal.{max u v}), BddAbove (Set.range f)

Ordinal.IsLimit.add

theorem Ordinal.IsLimit.add : ∀ (a : Ordinal.{u_4}) {b : Ordinal.{u_4}}, b.IsLimit → (a + b).IsLimit

Ordinal.IsNormal.le_iff

theorem Ordinal.IsNormal.le_iff : ∀ {f : Ordinal.{u_4} → Ordinal.{u_5}}, Ordinal.IsNormal f → ∀ {a b : Ordinal.{u_4}}, f a ≤ f b ↔ a ≤ b

Ordinal.one_add_omega

theorem Ordinal.one_add_omega : 1 + Ordinal.omega = Ordinal.omega

Ordinal.mul_add_div

theorem Ordinal.mul_add_div : ∀ (a : Ordinal.{u_4}) {b : Ordinal.{u_4}}, b ≠ 0 → ∀ (c : Ordinal.{u_4}), (b * a + c) / b = a + c / b

Ordinal.lsub_le_iff

theorem Ordinal.lsub_le_iff : ∀ {ι : Type u} {f : ι → Ordinal.{max u v}} {a : Ordinal.{max v u}}, Ordinal.lsub f ≤ a ↔ ∀ (i : ι), f i < a := by sorry

Ordinal.mul_succ

theorem Ordinal.mul_succ : ∀ (a b : Ordinal.{u_4}), a * Order.succ b = a * b + a

Ordinal.omega_isLimit

theorem Ordinal.omega_isLimit : Ordinal.omega.IsLimit

Ordinal.familyOfBFamily'.proof_1

theorem Ordinal.familyOfBFamily'.proof_1 : ∀ {ι : Type u_1} (r : ι → ι → Prop) [inst : IsWellOrder ι r] {o : Ordinal.{u_1}}, Ordinal.type r = o → ∀ (i : ι), Ordinal.typein r i < o

Ordinal.enumOrd_strictMono

theorem Ordinal.enumOrd_strictMono : ∀ {S : Set Ordinal.{u}}, Set.Unbounded (fun x x_1 => x < x_1) S → StrictMono (Ordinal.enumOrd S)

Ordinal.lt_omega

theorem Ordinal.lt_omega : ∀ {o : Ordinal.{u_1}}, o < Ordinal.omega ↔ ∃ n, o = ↑n

Ordinal.IsLimit.pos

theorem Ordinal.IsLimit.pos : ∀ {o : Ordinal.{u_4}}, o.IsLimit → 0 < o

Ordinal.mul_lt_mul_iff_left

theorem Ordinal.mul_lt_mul_iff_left : ∀ {a b c : Ordinal.{u_4}}, 0 < a → (a * b < a * c ↔ b < c)

`Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.10`

`Ordinal.enumOrd_surjective`

`Ordinal.mul_le_of_limit`

`Ordinal.mod_lt`

`Ordinal.lsub_le`

`Ordinal.div_zero`

`Ordinal.limitRecOn.proof_4`

`Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.39`

`not_small_ordinal`

`Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.2`

`Ordinal.sup_eq_bsup'`

`Ordinal.mul_isNormal`

`Ordinal.blsub_eq_lsub'`

`Ordinal.zero_or_succ_or_limit`

`Ordinal.omega_ne_zero`

`Ordinal.le_bsup`

`Ordinal.le_of_dvd`

`Ordinal.enumOrd_def'_nonempty`

`Ordinal.enumOrd_mem`

`Ordinal.sub_le`

`Ordinal.isNormal_iff_strictMono_limit`

`Ordinal.lt_sup`

`Ordinal.mod_one`

`Ordinal.sub_self`

`Ordinal.sup_le_lsub`

`Ordinal.succ_lt_of_not_succ`

`Ordinal.bddAbove_range`

`Ordinal.IsLimit.add`

`Ordinal.IsNormal.le_iff`

`Ordinal.one_add_omega`

`Ordinal.mul_add_div`

`Ordinal.lsub_le_iff`

`Ordinal.mul_succ`

`Ordinal.omega_isLimit`

`Ordinal.familyOfBFamily'.proof_1`

`Ordinal.enumOrd_strictMono`

`Ordinal.lt_omega`

`Ordinal.IsLimit.pos`

`Ordinal.mul_lt_mul_iff_left`

`Ordinal.enumOrd_def_nonempty`

`WellFounded.rank_lt_of_rel`

`Ordinal.div_nonempty`

`Ordinal.bsup_le`

`Ordinal.add_sub_cancel`

`Ordinal.lsub_not_mem_range`

`Ordinal.mex_not_mem_range`

`Ordinal.omega_pos`

`Ordinal.sub_nonempty`

`Ordinal.mul_lt_mul_of_pos_left`

`Ordinal.sup_eq_lsub_iff_succ`

`Ordinal.le_add_sub`

`Ordinal.div_lt`

`Ordinal.sup_le`

`Ordinal.sub_zero`

`Ordinal.IsNormal.lt_iff`

`Ordinal.bsup_le_iff`

`Mathlib.SetTheory.Ordinal.Arithmetic._auxLemma.44`

`Ordinal.le_sup`

`Ordinal.pred_eq_iff_not_succ`

`Ordinal.sub_le_self`

`Ordinal.lt_sub`

`Ordinal.bsup_le_blsub`

`Ordinal.limitRecOn.proof_2`

`Ordinal.lt_blsub`

`Ordinal.limitRecOn_succ`

`Ordinal.mul_div_le`

`Ordinal.IsNormal.eq_iff_zero_and_succ`

`Ordinal.sup_eq_bsup`

`Ordinal.IsNormal.isLimit`

`Ordinal.IsNormal.self_le`

`Ordinal.limit_le`

`Ordinal.div_add_mod`

`Ordinal.limitRecOn.proof_1`

`Ordinal.lsub_unique`