Ordinal.enum_lt_enum
theorem Ordinal.enum_lt_enum :
∀ {α : Type u} {r : α → α → Prop} [inst : IsWellOrder α r] {o₁ o₂ : Ordinal.{u}} (h₁ : o₁ < Ordinal.type r)
(h₂ : o₂ < Ordinal.type r), r (Ordinal.enum r o₁ h₁) (Ordinal.enum r o₂ h₂) ↔ o₁ < o₂
The theorem `Ordinal.enum_lt_enum` states that for any type `α` and a relation `r` on `α` that forms a well order, and for any two ordinals `o₁` and `o₂` that are less than the order type of `r`, the relation `r` orders the elements of `α` enumerated by `o₁` and `o₂` in the same way as the ordinals themselves. In other words, an element `x` of `α` that corresponds to `o₁` is less than an element `y` that corresponds to `o₂` under `r` if and only if the ordinal `o₁` is less than the ordinal `o₂`.
More concisely: For any well-ordered type `(α, r)` and ordinals `o₁` and `o₂` below its order type, `r(x₁ : α) ≤ r(x₂ : α)` if and only if `o₁` is less than `o₂` in the ordinal less-than relation.
|
Cardinal.mk_ordinal_out
theorem Cardinal.mk_ordinal_out : ∀ (o : Ordinal.{u_3}), Cardinal.mk (Quotient.out o).α = o.card
This theorem states that for any ordinal `o`, the cardinality of the type of elements (`α`) extracted from the equivalence class of `o` via the `Quotient.out` function (which is an implementation of the Axiom of Choice) equals to the cardinality of the ordinal `o` itself. In other words, the cardinal representation of the type of elements in the equivalence class of any ordinal is the same as the cardinality of that ordinal.
More concisely: For any ordinal `o`, the cardinality of `Quotient.out o` equals the cardinality of `o`.
|
Ordinal.nat_le_card
theorem Ordinal.nat_le_card : ∀ {o : Ordinal.{u_3}} {n : ℕ}, ↑n ≤ o.card ↔ ↑n ≤ o
This theorem states that for any ordinal `o` and natural number `n`, the cardinality of the ordinal `o` is greater than or equal to the natural number `n` if and only if the ordinal `o` is greater than or equal to the natural number `n` when both are considered as ordinals. In other words, a natural number is less than or equal to the cardinality of an ordinal if and only if it is also less than or equal to the ordinal itself when they are both cast to ordinals.
More concisely: For any ordinal `o` and natural number `n`, `o` has cardinality greater than or equal to `n` if and only if `o` is greater than or equal to `n` as ordinals.
|
Ordinal.typein_top
theorem Ordinal.typein_top :
∀ {α β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s]
(f : r ≺i s), Ordinal.typein s f.top = Ordinal.type r
The theorem `Ordinal.typein_top` states that for any two types `α` and `β` with well-ordering relations `r` and `s` respectively, and for any order-embedding `f` from `r` to `s`, the order type of the maximal element of `f` under `s` is equal to the order type of `r`. In simple terms, it implies that the order type of the "largest" element in the image of an order-embedding function is same as the order type of the initial well-ordered set. This is a fundamental property in the theory of ordinals.
More concisely: Given well-ordered types `α` and `β`, an order-embedding `f` from `α` to `β`, the order type of the maximal element of `f` under `β` equals the order type of `α`.
|
Ordinal.typein_one_out
theorem Ordinal.typein_one_out : ∀ (x : (Quotient.out 1).α), Ordinal.typein (fun x x_1 => x < x_1) x = 0
The theorem `Ordinal.typein_one_out` states that for every element `x` belonging to the set of equivalence classes represented by the number `1` under the operation `Quotient.out`, the order type of `x` with respect to the strict less than relation (`<`) is `0`. In other words, within the well-order defined by the less-than relation, `x` would be the first element (having an order type of `0`), for any `x` in the equivalence class of `1`.
More concisely: For every equivalence class represented by the number 1 under Quotient.out in the order type of well-founded relation <, the class's representative has order type 0.
|
Cardinal.lift_lt_univ'
theorem Cardinal.lift_lt_univ' : ∀ (c : Cardinal.{u}), Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v} := by
sorry
The theorem `Cardinal.lift_lt_univ'` states that for any cardinal number `c` in the universe `u`, when this cardinal number `c` is lifted to the higher universe `max (u + 1) v`, it is strictly less than the cardinality of the universe (denoted by 'Cardinal.univ'). In other words, the cardinality of any set (represented as a `Cardinal`) in a smaller universe is strictly less than the cardinality of the whole larger universe in which it is embedded.
More concisely: For any cardinal number `c` in universe `u`, `c` is strictly less than `Cardinal.univ` when lifted to the higher universe `max (u + 1) v`.
|
Cardinal.ord_zero
theorem Cardinal.ord_zero : Cardinal.ord 0 = 0
The theorem `Cardinal.ord_zero` states that the ordinal corresponding to the cardinal number 0 is also 0. In other words, the least ordinal number whose cardinal is 0 is 0 itself.
More concisely: The ordinal 0 is the cardinality of the empty set, and hence is itself a zero ordinal.
|
Ordinal.card_eq_nat
theorem Ordinal.card_eq_nat : ∀ {o : Ordinal.{u_3}} {n : ℕ}, o.card = ↑n ↔ o = ↑n
This theorem states that for any ordinal 'o' and natural number 'n', the cardinality of the ordinal 'o' is equal to the natural number 'n' if and only if the ordinal 'o' itself is 'n'. In other words, an ordinal is equal to a natural number if and only if its cardinality is that same number.
More concisely: For any ordinal 'o' and natural number 'n', 'o' has cardinality equal to 'n' if and only if 'o' is equal to the natural number 'n'.
|
Cardinal.lt_ord
theorem Cardinal.lt_ord : ∀ {c : Cardinal.{u_3}} {o : Ordinal.{u_3}}, o < c.ord ↔ o.card < c
The theorem `Cardinal.lt_ord` states that for any cardinal number `c` and any ordinal number `o`, `o` is less than the ordinal corresponding to `c` if and only if the cardinal of `o` is less than `c`. In other words, it establishes a relation between the cardinal and ordinal representations of a number, asserting that the ordinal representation of a cardinal is less than the cardinal if and only if the cardinal representation of the ordinal is less than the cardinal.
More concisely: For any cardinal number `c` and ordinal number `o`, `o` is an ordinal equivalent to the cardinality of a set with cardinality `c` if and only if `o` is strictly less than the ordinal corresponding to `c`.
|
WellOrder.wo
theorem WellOrder.wo : ∀ (self : WellOrder), IsWellOrder self.α self.r
This theorem states that for any given `WellOrder` instance, `r` is a well-ordering for the type `α`. In essence, it implies that `r` satisfies the properties of a well-ordering relation for the set `α`, i.e., it is a total order where every non-empty subset of `α` has a least element under the relation `r`.
More concisely: For any type `α` equipped with a `WellOrder` instance `r`, `r` is a well-ordering relation on `α`, i.e., it is a total order making every non-empty subset of `α` have a least element.
|
Cardinal.card_le_of_le_ord
theorem Cardinal.card_le_of_le_ord : ∀ {o : Ordinal.{u_3}} {c : Cardinal.{u_3}}, o ≤ c.ord → o.card ≤ c
This theorem states that for any ordinal `o` and any cardinal `c`, if `o` is less than or equal to the initial ordinal of cardinality `c`, then the cardinality of `o` is less than or equal to `c`. However, the reverse is not always true. For example, consider the case where `o` is ω+1 and `c` is ℵ₀.
More concisely: For any ordinal `o` and cardinal `c`, if `o` is a subset of the set of all ordinals of cardinality `c` (i.e., `o` has cardinality less than or equal to `c`), then the cardinality of `o` is less than or equal to `c`. However, not every cardinal `c` has an ordinal of cardinality `c` with this property.
|
Ordinal.type_lt
theorem Ordinal.type_lt : ∀ (o : Ordinal.{u_3}), (Ordinal.type fun x x_1 => x < x_1) = o
This theorem, `Ordinal.type_lt`, states that for every ordinal `o`, the order type of the well-ordering relation "less than" is `o`. In other words, for every well-order `o`, the structure that arises by considering the "less than" relation as a well-ordering on `o` is essentially the same as `o` itself, in the sense of order isomorphism. This theorem is a crucial result in the study of ordinals, as it provides a connection between a specific well-ordering relation and the general class of all well-orders.
More concisely: For every ordinal `o`, the well-ordering relation "less than" on `o` is order isomorphic to `o`.
|
Ordinal.pos_iff_ne_zero
theorem Ordinal.pos_iff_ne_zero : ∀ {o : Ordinal.{u_3}}, 0 < o ↔ o ≠ 0
The theorem `Ordinal.pos_iff_ne_zero` states that for any ordinal `o`, `o` is greater than zero if and only if `o` is not equal to zero. In other words, an ordinal number is positive if and only if it is not the zero ordinal. This theorem provides a characterization of positive ordinals in terms of non-zero ordinals.
More concisely: An ordinal is positive if and only if it is different from the zero ordinal.
|
Cardinal.ord_nat
theorem Cardinal.ord_nat : ∀ (n : ℕ), (↑n).ord = ↑n
The theorem `Cardinal.ord_nat` states that for all natural numbers `n`, the ordinal corresponding to the cardinal of `n` is equal to `n`. In mathematical terms, it signifies that the cardinality-to-ordinal mapping for natural numbers is the identity function.
More concisely: The theorem `Cardinal.ord_nat` asserts that the ordinal representation of a natural number equals the number itself.
|
Cardinal.lt_univ'
theorem Cardinal.lt_univ' :
∀ {c : Cardinal.{max (u + 1) v}}, c < Cardinal.univ.{u, v} ↔ ∃ c', c = Cardinal.lift.{max (u + 1) v, u} c' := by
sorry
The theorem `Cardinal.lt_univ'` states that for any cardinal number `c` in either the `u + 1` or `v` universe, `c` is less than the cardinality of the universe (`Cardinal.univ`) if and only if there exists another cardinal number `c'` such that `c` is the universe lift of `c'`. In other words, a cardinal number `c` is smaller than the cardinality of the universe if and only if `c` can be obtained by lifting a cardinal number from a smaller universe to the current universe. This theorem is a characterization of the order relationship between a cardinal number and the cardinality of the universe in terms of the universe lift operation on cardinals.
More concisely: A cardinal number `c` is smaller than the cardinality of the universe if and only if it is the universe lift of some cardinal number in a smaller universe.
|
Ordinal.card_add
theorem Ordinal.card_add : ∀ (o₁ o₂ : Ordinal.{u_3}), (o₁ + o₂).card = o₁.card + o₂.card
This theorem states that for any two ordinals `o₁` and `o₂`, the cardinality of the sum of `o₁` and `o₂` is equal to the sum of the cardinalities of `o₁` and `o₂`. In other words, the operation of taking the cardinality of an ordinal commutes with the addition of ordinals. This is analogous to the cardinality of the union of two disjoint sets being equal to the sum of their cardinalities in set theory.
More concisely: The cardinality of the sum of two ordinals is equal to the sum of their cardinalities.
|
Ordinal.enum_typein
theorem Ordinal.enum_typein :
∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] (a : α), Ordinal.enum r (Ordinal.typein r a) ⋯ = a := by
sorry
The theorem `Ordinal.enum_typein` states that for any type `α` and a relation `r` on `α` which forms a well-order, and for any element `a` of type `α`, when we compute the ordinal type of `a` relative to `r` using the `Ordinal.typein` function, and then use this ordinal to enumerate the elements of `α` in the order dictated by `r` using the `Ordinal.enum` function, we get back the same element `a`. In other words, the processes of computing the ordinal type of an element and enumerating elements of a well-ordered set according to their ordinal types are inverses of each other under this well-ordering.
More concisely: For any well-ordered type `(α, r)` and element `a` of `α`, `Ordinal.enum (Ordinal.typein r a) = a`.
|
Ordinal.lift_card
theorem Ordinal.lift_card : ∀ (a : Ordinal.{v}), Cardinal.lift.{u, v} a.card = (Ordinal.lift.{u, v} a).card
The theorem `Ordinal.lift_card` states that for any ordinal `a`, lifting the cardinality of `a` (using the universe lift operation on cardinals) is equivalent to first lifting the ordinal `a` to a higher universe and then taking its cardinality. In mathematical terms, it means that the two operations - lifting the cardinality and lifting the ordinal - commute with each other.
More concisely: For any ordinal `a`, the lifted cardinality of `a` is equal to the cardinality of the lifted ordinal `a`.
|
Ordinal.one_le_iff_pos
theorem Ordinal.one_le_iff_pos : ∀ {o : Ordinal.{u_3}}, 1 ≤ o ↔ 0 < o
This theorem, `Ordinal.one_le_iff_pos`, states that for all ordinals `o`, the ordinal '1' is less than or equal to `o` if and only if the ordinal '0' is less than `o`. In other words, in the context of ordinals, the statements "1 is less than or equal to `o`" and "0 is less than `o`" are equivalent. This theorem is at the heart of understanding orderings in the ordinals.
More concisely: For all ordinals `o`, 1 ≤ o if and only if 0 < o.
|
Ordinal.le_add_right
theorem Ordinal.le_add_right : ∀ (a b : Ordinal.{u_3}), a ≤ a + b
This theorem, `Ordinal.le_add_right`, asserts that for all ordinal numbers `a` and `b`, `a` is always less than or equal to the sum of `a` and `b`. This is an analogue to a common arithmetic law in the context of ordinal numbers, where an ordinal number `a` added to any other ordinal number `b` results in a sum that is greater or equal to `a`. This can be written in mathematical terms as ∀a,b ∈ Ordinal, a ≤ a + b.
More concisely: For all ordinal numbers `a` and `b`, `a` is less than or equal to the sum `a + b`.
|
Cardinal.ord_card_le
theorem Cardinal.ord_card_le : ∀ (o : Ordinal.{u_3}), o.card.ord ≤ o
This theorem states that for any ordinal `o`, the cardinality of the ordinal `o` (which is obtained by mapping the ordinal to a cardinal using `Ordinal.card`) when mapped back to an ordinal using `Cardinal.ord` is always less than or equal to the original ordinal `o`. In other words, the process of going from an ordinal to its cardinality and back again does not increase the size of the ordinal. In mathematical terms, for all ordinals `o`, the operation `Cardinal.ord (Ordinal.card o)` yields a value that is less than or equal to `o`.
More concisely: For every ordinal `o`, the cardinality of `o` (as a cardinal number) is less than or equal to `o` as an ordinal number.
|
Ordinal.lift_id
theorem Ordinal.lift_id : ∀ (a : Ordinal.{u}), Ordinal.lift.{u, u} a = a
The theorem `Ordinal.lift_id` states that for any ordinal `a` in a given universe `u`, lifting `a` to the same universe `u` (i.e., applying the universe lift operation `Ordinal.lift` with both source and target universes being `u`) results in `a` itself. In other words, the operation of lifting an ordinal to its own universe is an identity operation. This is a structural property of ordinals in the context of set theory in Lean 4.
More concisely: For any ordinal `a` in universe `u`, `Ordinal.lift a u a` holds, or equivalently, applying the `Ordinal.lift` operation with source and target universes equal to `u` results in the identity on ordinals.
|
Ordinal.lift_lt
theorem Ordinal.lift_lt : ∀ {a b : Ordinal.{v}}, Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} b ↔ a < b
The theorem `Ordinal.lift_lt` states that for any two ordinals `a` and `b` in a universe `v`, the ordinal `a` is less than the ordinal `b` if and only if the lift of the ordinal `a` to a larger universe `max v u` is less than the lift of the ordinal `b` to the same larger universe. This theorem establishes the preservation of order relationships under the universe lift operation for ordinals.
More concisely: For any ordinals `a` and `b` in a universe `v`, `a < b` if and only if the lifted ordinals `Ordinal.lift a max v` and `Ordinal.lift b max v` satisfy `Ordinal.lift a max v < Ordinal.lift b max v` in the larger universe `max v`.
|
Ordinal.add_succ
theorem Ordinal.add_succ : ∀ (o₁ o₂ : Ordinal.{u_3}), o₁ + Order.succ o₂ = Order.succ (o₁ + o₂)
This theorem states that for any two ordinals `o₁` and `o₂`, the sum of `o₁` and the successor of `o₂` is equal to the successor of the sum of `o₁` and `o₂`. In other words, if you add one (using the `Order.succ` function) to the second operand of the addition, it is the same as adding the operands first and then adding one to the result. This is a property of ordinal arithmetic that mirrors similar properties in standard arithmetic.
More concisely: For any ordinals `o₁` and `o₂`, `Order.succ (o₁ + o₂) = o₁ + Order.succ o₂`.
|
Cardinal.gc_ord_card
theorem Cardinal.gc_ord_card : GaloisConnection Cardinal.ord Ordinal.card
The theorem `Cardinal.gc_ord_card` states that there exists a Galois connection between the function `Cardinal.ord` and `Ordinal.card`. In other words, for any cardinal number `c` and ordinal number `o`, the ordinal corresponding to `c` is less than or equal to `o` if and only if `c` is less than or equal to the cardinal of `o`. Here, `Cardinal.ord` assigns to a cardinal `c` the least ordinal whose cardinal is `c`, and `Ordinal.card` gives the cardinality of any type on which a relation with the given ordinal order type is defined.
More concisely: The theorem `Cardinal.gc_ord_card` asserts that the functions `Cardinal.ord` and `Ordinal.card` define a Galois connection, meaning that for all cardinals `c` and ordinals `o`, `Cardinal.ord c ≤ o` if and only if `c ≤ Ordinal.card o`.
|
Ordinal.add_one_eq_succ
theorem Ordinal.add_one_eq_succ : ∀ (o : Ordinal.{u_3}), o + 1 = Order.succ o
The theorem `Ordinal.add_one_eq_succ` states that for every well-order `o` of type ordinal, adding one to `o` is equivalent to the successor of `o`. In other words, the operation of incrementing an ordinal by one results in the same ordinal as invoking the successor function on that ordinal. This holds regardless of whether the original ordinal `o` was maximal or not.
More concisely: For every well-ordered ordinal `o`, `o + 1` equals the successor of `o`.
|
Ordinal.le_one_iff
theorem Ordinal.le_one_iff : ∀ {a : Ordinal.{u_3}}, a ≤ 1 ↔ a = 0 ∨ a = 1
The theorem `Ordinal.le_one_iff` states that for any ordinal `a`, `a` is less than or equal to 1 if and only if `a` is equal to 0 or `a` is equal to 1. In other words, in the context of ordinals, the only values that are less than or equal to 1 are 0 and 1 itself.
More concisely: For any ordinal `a`, `a <= 1` if and only if `a = 0` or `a = 1`.
|
Ordinal.typein_lt_typein
theorem Ordinal.typein_lt_typein :
∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] {a b : α},
Ordinal.typein r a < Ordinal.typein r b ↔ r a b
The theorem `Ordinal.typein_lt_typein` states that for any type `α` and a relation `r` on `α` that is a well-order, and any two elements `a` and `b` from `α`, the ordinal type of `a` with respect to `r` is less than the ordinal type of `b` with respect to `r` if and only if `r a b` holds. In other words, the ordering of the ordinal types of elements (defined by `Ordinal.typein`) reflects the ordering in the well-order `r`.
More concisely: For any well-ordered type `(α, r)`, the ordinal type `Ordinal.typein a` of an element `a` is less than the ordinal type `Ordinal.typein b` of another element `b` if and only if `r a b` holds.
|
Ordinal.out_nonempty_iff_ne_zero
theorem Ordinal.out_nonempty_iff_ne_zero : ∀ {o : Ordinal.{u_3}}, Nonempty (Quotient.out o).α ↔ o ≠ 0
The theorem `Ordinal.out_nonempty_iff_ne_zero` states that for any ordinal `o`, there exists some element in the set that `o` (considered as an equivalence class) represents if and only if `o` is not equal to zero. In other words, an ordinal number has a non-empty set representation if and only if it is not zero.
More concisely: An ordinal is non-empty if and only if it is not equal to zero.
|
Ordinal.nat_lt_card
theorem Ordinal.nat_lt_card : ∀ {o : Ordinal.{u_3}} {n : ℕ}, ↑n < o.card ↔ ↑n < o
The theorem `Ordinal.nat_lt_card` states that for any ordinal `o` and natural number `n`, the cardinality of the ordinal `n` is less than the cardinal of the ordinal `o` if and only if the ordinal `n` is less than the ordinal `o`. Essentially, it shows that the inequality relationship between two natural numbers, when lifted to the level of their corresponding ordinals, corresponds directly to the inequality relationship between their cardinalities.
More concisely: For any ordinal numbers `o` and `n`, `n < o` if and only if the cardinality of `n` is less than the cardinality of `o`.
|
Ordinal.not_lt_zero
theorem Ordinal.not_lt_zero : ∀ (o : Ordinal.{u_3}), ¬o < 0
This theorem states that for any ordinal 'o', it is not possible for 'o' to be less than zero. In other words, no ordinal number is less than zero.
More concisely: No ordinal is less than zero.
|
Cardinal.ord_injective
theorem Cardinal.ord_injective : Function.Injective Cardinal.ord
The theorem `Cardinal.ord_injective` is stating that the function `Cardinal.ord` is injective. In the context of mathematics, this means that for any two cardinals `c1` and `c2`, if `Cardinal.ord c1` is equal to `Cardinal.ord c2`, then `c1` must be equal to `c2`. In other words, no two different cardinals can have the same ordinal under the `Cardinal.ord` function. The function `Cardinal.ord` assigns to each cardinal number the least ordinal number whose cardinal is that cardinal number, so this theorem is ensuring the uniqueness of this assignment.
More concisely: The `Cardinal.ord` function maps distinct cardinal numbers to distinct ordinal numbers.
|
Ordinal.lift_down
theorem Ordinal.lift_down :
∀ {a : Ordinal.{u}} {b : Ordinal.{max u v}}, b ≤ Ordinal.lift.{v, u} a → ∃ a', Ordinal.lift.{v, u} a' = b := by
sorry
The theorem `Ordinal.lift_down` states that for any two ordinals `a` and `b`, where `a` is of type `Ordinal.{u}` and `b` is of type `Ordinal.{max u v}`, if `b` is less than or equal to the ordinal obtained by lifting `a` (i.e. `Ordinal.lift.{v, u} a`), then there exists another ordinal `a'` such that the ordinal obtained by lifting `a'` is equal to `b`. In simpler terms, this theorem guarantees a "down" operation for every "lift" operation on ordinals, provided the lifted ordinal is greater than or equal to the original ordinal.
More concisely: For any ordinals `a` of type `Ordinal.{u}` and `b` of type `Ordinal.{max u v}`, if `b <= Ordinal.lift.{v, u} a`, then there exists an ordinal `a'` such that `Ordinal.lift.{v, u} a' = b`.
|
Ordinal.card_type
theorem Ordinal.card_type :
∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r], (Ordinal.type r).card = Cardinal.mk α
The theorem `Ordinal.card_type` states that for any type `α` and a relation `r` on `α` that forms a well order, the cardinality of the ordinal corresponding to the order type `r` is equal to the cardinal number of the type `α`. In layman's terms, it says that the size (cardinality) of the set of order types of well-orders on a type `α` is the same as the size of the set `α` itself.
More concisely: For any type `α` and well-order `r` on `α`, the order type `r` has the same cardinality as `α`.
|
Ordinal.zero_le
theorem Ordinal.zero_le : ∀ (o : Ordinal.{u_3}), 0 ≤ o
This theorem states that for any ordinal `o`, zero is less than or equal to `o`. In other words, in the class of well orders, the ordinal zero is less than or equal to every other ordinal.
More concisely: For any ordinal `o`, zero is less than or equal to `o` (or equivalently, `0 <= o`).
|
Ordinal.one_ne_zero
theorem Ordinal.one_ne_zero : 1 ≠ 0
This theorem states that the ordinal number one is not equal to zero. In other words, it asserts that one and zero are distinct values in the context of ordinal numbers, which are a type of number system used to represent order or position.
More concisely: One is not equal to zero in the ordinal number system.
|
Ordinal.typein_lt_self
theorem Ordinal.typein_lt_self :
∀ {o : Ordinal.{u_3}} (i : (Quotient.out o).α), Ordinal.typein (fun x x_1 => x < x_1) i < o
The theorem `Ordinal.typein_lt_self` states that for any ordinal `o` and any element `i` from the underlying set of the well-ordered set represented by `o`, the order type of `i` with respect to the less than relation (i.e., `Ordinal.typein (fun x x_1 => x < x_1) i`) is strictly less than `o` itself. This essentially means that the order type of an element within a well-ordered set, when considering only elements less than it, is always strictly less than the order type of the entire set.
More concisely: For any well-ordered set (ordinal) `o` and any element `i` in `o`, the order type of `i` is strictly less than the order type of `o`.
|
Cardinal.card_ord
theorem Cardinal.card_ord : ∀ (c : Cardinal.{u_3}), c.ord.card = c
The theorem `Cardinal.card_ord` states that for any cardinal number `c`, the cardinality of the ordinal number corresponding to `c` (obtained via the function `Cardinal.ord`), is `c` itself. In other words, the cardinality function `Ordinal.card` and the ordinal function `Cardinal.ord` are inverses of each other when applied to a cardinal number `c`.
More concisely: For any cardinal number `c`, the ordinal number obtained from `Cardinal.ord(c)` has cardinality `c`. In other words, `Cardinal.ord` and `Ordinal.card` are inverses of each other when applied to cardinal numbers.
|
Ordinal.lift_uzero
theorem Ordinal.lift_uzero : ∀ (a : Ordinal.{u}), Ordinal.lift.{0, u} a = a
This theorem states that for any ordinal `a` from some universe `u`, when this ordinal `a` is lifted to the zero universe, it remains unchanged. In other words, the operation of lifting an ordinal to the zero universe is essentially an identity operation: it doesn't alter the ordinal.
More concisely: For any ordinal `a` in some universe, the lifted ordinal in the zero universe is equal to the original ordinal `a`.
|
Ordinal.le_add_left
theorem Ordinal.le_add_left : ∀ (a b : Ordinal.{u_3}), a ≤ b + a
This theorem states that for any two ordinals 'a' and 'b', the ordinal 'a' is always less than or equal to the sum of 'b' and 'a'. In other words, given any two ordinals, the value of an ordinal is always less than or equal to the value of the sum of that ordinal and another ordinal. This is a property of ordinals in the mathematical field of set theory.
More concisely: For any ordinals 'a' and 'b', a ≤ a + b.
|
Ordinal.type_ne_zero_iff_nonempty
theorem Ordinal.type_ne_zero_iff_nonempty :
∀ {α : Type u} {r : α → α → Prop} [inst : IsWellOrder α r], Ordinal.type r ≠ 0 ↔ Nonempty α
The theorem `Ordinal.type_ne_zero_iff_nonempty` states that for any type `α` and any relation `r` on `α`, if `α` is a well-ordered set under the relation `r` (as expressed by the instance `IsWellOrder α r`), then the order type of the well order (i.e., `Ordinal.type r`) is not equal to zero if and only if `α` is a nonempty set. In other words, a well-ordered set has a non-zero order type if and only if the set itself is not empty.
More concisely: A well-ordered set is non-empty if and only if its order type is non-zero.
|
Ordinal.le_zero
theorem Ordinal.le_zero : ∀ {o : Ordinal.{u_3}}, o ≤ 0 ↔ o = 0
The theorem `Ordinal.le_zero` states that for any ordinal `o` in the universe `u_3`, `o` is less than or equal to zero if and only if `o` is equal to zero. This theorem reflects that in the context of ordinals, there is no ordinal number less than zero. In other words, zero is the smallest ordinal number.
More concisely: For any ordinal number `o`, `o <= 0` if and only if `o = 0`.
|
Ordinal.succ_ne_zero
theorem Ordinal.succ_ne_zero : ∀ (o : Ordinal.{u_3}), Order.succ o ≠ 0
The theorem `Ordinal.succ_ne_zero` states that for any ordinal `o`, the successor of `o` is not equal to zero. In other words, in the context of ordinals, which represent well orders, the next ordinal after any given ordinal is always non-zero. This is true regardless of the specific ordering or type of the ordinal.
More concisely: For any ordinal `o`, `o.succ ≠ 0`.
|
Cardinal.ord_le
theorem Cardinal.ord_le : ∀ {c : Cardinal.{u_3}} {o : Ordinal.{u_3}}, c.ord ≤ o ↔ c ≤ o.card
This theorem, `Cardinal.ord_le`, states that for any cardinal `c` and any ordinal `o`, the ordinal corresponding to `c` (i.e., the least ordinal whose cardinal is `c`) is less than or equal to `o` if and only if `c` is less than or equal to the cardinal of `o` (i.e., the cardinality of any type on which a relation with order type `o` is defined). This connects the concepts of cardinal and ordinal numbers in a fundamental way, showing that their orders align under certain conditions.
More concisely: The ordinal representing a cardinal is less than or equal to an ordinal `o` if and only if the cardinal is less than or equal to the cardinality of the type carrying `o`'s order structure.
|
Ordinal.type_eq_zero_of_empty
theorem Ordinal.type_eq_zero_of_empty :
∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] [inst_1 : IsEmpty α], Ordinal.type r = 0
The theorem `Ordinal.type_eq_zero_of_empty` states that for any type `α` and any relation `r` on `α`, if `α` is a well-ordered set (as defined by the `IsWellOrder` instance) and also an empty set (as defined by the `IsEmpty` instance), then the ordinal number corresponding to this well-order, denoted as `Ordinal.type r`, is equal to zero. This is because the ordinal of an empty set is defined to be zero.
More concisely: If a well-ordered and empty set `α` has a corresponding ordinal number, then this ordinal number is equal to zero.
|
Ordinal.out_empty_iff_eq_zero
theorem Ordinal.out_empty_iff_eq_zero : ∀ {o : Ordinal.{u_3}}, IsEmpty (Quotient.out o).α ↔ o = 0
This theorem establishes a relationship between the type of well orders and the concept of emptiness. It states that for any well order 'o' of a certain type, the set of elements 'α' chosen from the equivalence class of 'o' is empty if and only if 'o' is the zero ordinal. This theorem essentially links the property of a well order being equivalent to the zero ordinal with the absence of elements in its equivalence class.
More concisely: For any well order 'o', the equivalence class of 'o' is empty if and only if 'o' is the zero ordinal.
|
Ordinal.one_le_iff_ne_zero
theorem Ordinal.one_le_iff_ne_zero : ∀ {o : Ordinal.{u_3}}, 1 ≤ o ↔ o ≠ 0
This theorem states that for any ordinal 'o', 'o' is greater than or equal to 1 if and only if 'o' is not equal to 0. This is saying in other words that an ordinal number is non-zero exactly when it is at least 1. This is a property of ordinal numbers which are used to represent order types in type theory, where order types are equivalence classes of well-orders.
More concisely: For any ordinal number 'o', o is non-zero if and only if o ≥ 1.
|
RelIso.ordinal_type_eq
theorem RelIso.ordinal_type_eq :
∀ {α β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s],
r ≃r s → Ordinal.type r = Ordinal.type s
This theorem asserts that for any two types `α` and `β` with respective relations `r` and `s`, both of which are well-ordered (as denoted by `IsWellOrder α r` and `IsWellOrder β s`), if there is a relation-preserving isomorphism (`≃r`) between `r` and `s`, then the ordinal types of `r` and `s` (given by `Ordinal.type r` and `Ordinal.type s`) are equal. Essentially, it says that isomorphic well-orders yield the same ordinal type.
More concisely: If two well-ordered types `α` and `β` have isomorphic relations `r` and `s`, then their ordinal types `Ordinal.type r` and `Ordinal.type s` are equal.
|
Ordinal.lt_one_iff_zero
theorem Ordinal.lt_one_iff_zero : ∀ {a : Ordinal.{u_3}}, a < 1 ↔ a = 0
The theorem `Ordinal.lt_one_iff_zero` states that for any ordinal `a` from the universe `u_3`, `a` is less than 1 if and only if `a` is exactly 0. In other words, in the context of ordinals, the only ordinal number that is less than 1 is 0 itself.
More concisely: For any ordinal number `a`, `a` is less than 1 if and only if `a` equals 0.
|
Ordinal.lift_umax
theorem Ordinal.lift_umax : Ordinal.lift.{max u v, u} = Ordinal.lift.{v, u}
The theorem `Ordinal.lift_umax` states that the "lift" operation on ordinals is commutative with respect to the maximum of two universe levels. Specifically, lifting an ordinal from universe level `u` to the maximum of `u` and `v` is the same as lifting it directly to universe level `v`. This theorem ensures the consistency of ordinal lifting across different universe levels.
More concisely: For any ordinal `α` and universes `u` and `v` such that `u <= v`, the lift of `α` from `u` to `u` is equal to its lift from `u` to `v`.
|
Ordinal.succ_zero
theorem Ordinal.succ_zero : Order.succ 0 = 1
The theorem `Ordinal.succ_zero` states that the successor of zero, in an ordered set that respects the successor relationship, is one. In other words, if you've defined an ordering on a type and the operations of 'successor' in that order, then moving one step from zero in the positive direction will result in one.
More concisely: In an ordered set, the successor of zero is one.
|
Ordinal.lift_id'
theorem Ordinal.lift_id' : ∀ (a : Ordinal.{max u_3 u_4}), Ordinal.lift.{u_3, max u_3 u_4} a = a
The theorem `Ordinal.lift_id'` states that for any ordinal `a` in a universe that is either equal to or lower than a given universe, the operation of lifting this ordinal to its own universe, or to a universe which is equivalent or higher, will result in the ordinal itself. This underlines the property that the lifting operation does not change the ordinal if the target universe is not strictly higher than the original universe of the ordinal.
More concisely: For any ordinal `a` in a given universe, `Ordinal.lift_id a` equals `a`.
|
Cardinal.ord_lt_ord
theorem Cardinal.ord_lt_ord : ∀ {c₁ c₂ : Cardinal.{u_3}}, c₁.ord < c₂.ord ↔ c₁ < c₂
This theorem, `Cardinal.ord_lt_ord`, states that for any two cardinal numbers `c₁` and `c₂` in the same type `u_3`, the ordinal number corresponding to `c₁` is less than the ordinal number corresponding to `c₂` if and only if `c₁` is less than `c₂`. In other words, the ordering of ordinals corresponding to two cardinals reflects the ordering of the cardinals themselves.
More concisely: The ordinal numbers corresponding to two cardinal numbers are ordered similarly if and only if the cardinal numbers are ordered similarly.
|
Ordinal.type_nat_lt
theorem Ordinal.type_nat_lt : (Ordinal.type fun x x_1 => x < x_1) = Ordinal.omega
This theorem states that the order type of the natural numbers, where the order is defined by the less-than relation, is equal to the first infinite ordinal, often represented as ω. In essence, it establishes that the ordering of natural numbers corresponds to the initial countably infinite ordinal. It's important to note that using this theorem in simplifications with `simp [omega]` can cause an infinite loop in proof verification.
More concisely: The natural numbers, ordered by the less-than relation, have the same order type as the first infinite ordinal ω.
|
Ordinal.typein_lt_type
theorem Ordinal.typein_lt_type :
∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] (a : α), Ordinal.typein r a < Ordinal.type r
This theorem states that for any type `α`, along with a relation `r` on `α` that forms a well-order, and for any element `a` of `α`, the ordinal type of `a` with respect to the relation `r` (`Ordinal.typein r a`) is strictly less than the ordinal type of the well-ordered set itself (`Ordinal.type r`). In other words, the order type of an element in a well-ordered set is always less than the order type of the entire well-ordered set.
More concisely: For any well-ordered type `(α, r)`, the ordinal type of any element `a` is strictly less than the ordinal type of the well-ordered set `α` with respect to the relation `r`.
|
Ordinal.typein_enum
theorem Ordinal.typein_enum :
∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] {o : Ordinal.{u}} (h : o < Ordinal.type r),
Ordinal.typein r (Ordinal.enum r o h) = o
The theorem `Ordinal.typein_enum` states that for any well-ordered set `α` with a well-ordering relation `r`, and for any ordinal `o` that is less than the order type of the relation `r`, the order type of an element (specified by the function `Ordinal.enum`) in the well order is equal to the ordinal `o` itself. In simpler terms, the function `Ordinal.typein` when applied to an element of the well-ordered set, which is obtained via the function `Ordinal.enum` using an ordinal `o`, will return the same ordinal `o`.
More concisely: For any well-ordered set `(α, r)` and ordinal `o < |r|`, `Ordinal.typein (Ordinal.enum r o α) = o`.
|
Ordinal.card_one
theorem Ordinal.card_one : Ordinal.card 1 = 1
The theorem `Ordinal.card_one` states that the cardinality of the ordinal number 1 is 1. In other words, any type with a well-order relation that has the order type of the ordinal 1 (which in essence is a singleton set) has exactly one element.
More concisely: The theorem `Ordinal.card_1` asserts that the ordinal number 1 has cardinality 1.
|
Ordinal.succ_one
theorem Ordinal.succ_one : Order.succ 1 = 2
This theorem asserts that the successor of the number one in any ordered structure, where the successor operation is defined, is the number two. In other words, for any preorder structure that also has a successor order, when the successor operation is applied to the number one, the result will always be the number two.
More concisely: In any preorder structure with a successor operation, the successor of 1 is equal to 2.
|
Ordinal.type_eq
theorem Ordinal.type_eq :
∀ {α β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s],
Ordinal.type r = Ordinal.type s ↔ Nonempty (r ≃r s)
The theorem `Ordinal.type_eq` states that for any two types `α` and `β` with properties `r` and `s` respectively, that are well-ordered (meaning that every non-empty subset has a least element), the ordinal type of `r` is equal to the ordinal type of `s` if and only if there exists a nonempty order isomorphism between `r` and `s`. An order isomorphism `r ≃r s` is a bijective function that preserves order relations, meaning that for all elements `a` and `b`, `a` is related to `b` under `r` if and only if the image of `a` under the isomorphism is related to the image of `b` under `s`.
More concisely: For well-ordered types `α` and `β` with order isomorphisms `r ≃s`, the ordinal types of `α` under relation `r` and `β` under relation `s` are equal.
|
Cardinal.ord_eq
theorem Cardinal.ord_eq : ∀ (α : Type u_3), ∃ r, ∃ (wo : IsWellOrder α r), (Cardinal.mk α).ord = Ordinal.type r := by
sorry
The theorem `Cardinal.ord_eq` asserts that for every type `α`, there exists a relation `r` and a proof that the relation `r` is a well-order on `α` such that the ordinal corresponding to the cardinality of `α` (as computed by `Cardinal.ord (Cardinal.mk α)`) is equal to the order type of the relation `r` (as computed by `Ordinal.type r`). In simpler terms, it says that every cardinal number has an associated ordinal number that is determined by a specific well-ordering on its underlying type.
More concisely: For every type `α`, there exists a well-order `r` on `α` such that the ordinal type of `r` equals the cardinality of `α`.
|
Ordinal.lt_wf
theorem Ordinal.lt_wf : WellFounded fun x x_1 => x < x_1
This theorem states that the less-than relation ("<") on ordinals is well-founded. In the context of set theory, an ordinal is a set that is well-ordered by set membership. A relation is well-founded if there are no infinite descending chains. So, this theorem essentially says that it's impossible to find an infinite sequence of ordinals where each ordinal is smaller than the previous one.
More concisely: The less-than relation on ordinals is a well-founded relation.
|
Ordinal.card_zero
theorem Ordinal.card_zero : Ordinal.card 0 = 0
This theorem states that the cardinality of the ordinal zero is zero. In other words, a type that has a well-ordering relation equivalent to the order type of the ordinal zero has a cardinality, or size, of zero. In terms of set theory, it's saying that the set with no elements (the empty set) has a cardinality of zero.
More concisely: The ordinal zero has cardinality 0. In set theory, the empty set has cardinality 0.
|
Ordinal.eq_zero_or_pos
theorem Ordinal.eq_zero_or_pos : ∀ (a : Ordinal.{u_3}), a = 0 ∨ 0 < a
The theorem `Ordinal.eq_zero_or_pos` states that for any ordinal `a` of type `Ordinal`, `a` is either equal to zero or greater than zero. In other words, this theorem asserts that any ordinal number is either zero or a positive number.
More concisely: For any ordinal number `a`, `a` is equal to zero or greater than zero.
|
Cardinal.ord_le_ord
theorem Cardinal.ord_le_ord : ∀ {c₁ c₂ : Cardinal.{u_3}}, c₁.ord ≤ c₂.ord ↔ c₁ ≤ c₂
The theorem `Cardinal.ord_le_ord` states that for any two cardinals `c₁` and `c₂`, the ordinal of `c₁` is less than or equal to the ordinal of `c₂` if and only if `c₁` is less than or equal to `c₂`. In other words, the ordering of cardinals respects the ordering of their corresponding ordinals. This theorem provides a connection between the order of cardinal numbers and the order of their corresponding ordinal numbers.
More concisely: For any cardinals `c₁` and `c₂`, `Cardinal.ord c₁ ≤ Cardinal.ord c₂` if and only if `c₁ ≤ c₂`.
|
Ordinal.induction
theorem Ordinal.induction :
∀ {p : Ordinal.{u} → Prop} (i : Ordinal.{u}), (∀ (j : Ordinal.{u}), (∀ k < j, p k) → p j) → p i
This theorem provides a formulation of well-founded induction on ordinals which is compatible with the `induction` tactic in Lean 4. This theorem states that for any property `p` and any ordinal `i`, if the property `p` holds for every ordinal `j` where `p` holds for all ordinals `k` less than `j`, then `p` also holds for the ordinal `i`. In other words, this theorem asserts that if a property is true for all smaller ordinals, then it is also true for the ordinal under consideration.
More concisely: The theorem asserts that any property holding for all ordinals below a given ordinal also holds for that ordinal in the well-founded relation.
|
Ordinal.inductionOn
theorem Ordinal.inductionOn :
∀ {C : Ordinal.{u_3} → Prop} (o : Ordinal.{u_3}),
(∀ (α : Type u_3) (r : α → α → Prop) [inst : IsWellOrder α r], C (Ordinal.type r)) → C o
The theorem `Ordinal.inductionOn` is a principle of mathematical induction for ordinals. For any property `C` and any ordinal `o`, if for all well-ordered types `α` and relations `r` on `α` (which is a well-order), the property `C` holds on the ordinal type of `r`, then the property `C` holds on `o`. Essentially, this theorem states that if a property is true for all well-orders, then it is true for all ordinals.
More concisely: If a property holds for all well-ordered types and relations, then it holds for any ordinal.
|
Ordinal.lift_umax'
theorem Ordinal.lift_umax' : Ordinal.lift.{max v u, u} = Ordinal.lift.{v, u}
The theorem `Ordinal.lift_umax'` states that the operations of lifting ordinals from a universe of type `u` to a universe of type `max v u` and lifting from a universe of type `u` to a universe of type `v` are the same. In other words, it doesn't matter whether we first lift an ordinal to a universe of a larger type and then lift it to the maximum of that type and another type, or whether we directly lift it to the maximum type. The result will be the same in either case.
More concisely: For any ordinal `α` and universes `u` and `v` with `u ≤ max v u`, the ordinal lifting functions from `u` to `max v u` and from `u` to `v` are equal: `Ordinal.lift u α max v u = Ordinal.lift u α v`.
|
Ordinal.lift_inj
theorem Ordinal.lift_inj : ∀ {a b : Ordinal.{v}}, Ordinal.lift.{u, v} a = Ordinal.lift.{u, v} b ↔ a = b
The theorem `Ordinal.lift_inj` states that for any two ordinals `a` and `b` in the universe `v`, the lift operation `Ordinal.lift` which embeds `Ordinal.v` as a proper initial segment of `Ordinal.{max v u}` for `u > v`, is injective. This means, `Ordinal.lift` applied to `a` equals `Ordinal.lift` applied to `b` if and only if `a` equals `b`. This ensures the uniqueness of the lift operation's result, implying no two different ordinals can have the same lift.
More concisely: The `Ordinal.lift` function maps distinct ordinals to distinct lifted ordinals in `Ordinal.{max v u}`.
|