Cardinal.beth_limit
theorem Cardinal.beth_limit : ∀ {o : Ordinal.{u_1}}, o.IsLimit → Cardinal.beth o = ⨆ a, Cardinal.beth ↑a
The theorem `Cardinal.beth_limit` states that for any limit ordinal `o`, the beth number of `o` is the supremum of the beth numbers of all ordinals less than `o`. In other words, if `o` is a limit ordinal (an ordinal which is not zero and not a successor), then the beth number of `o` (denoted as `beth o`) is equal to the supremum (denoted as `⨆ a`) of the beth number of `a` for all `a` less than `o`. This is a characterization of beth numbers at limit ordinals in the context of the generalized continuum hypothesis.
More concisely: For any limit ordinal `o`, the beth number `beth o` is the supremum of the beth numbers of all ordinals less than `o`.
|
Cardinal.ord_isLimit
theorem Cardinal.ord_isLimit : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → c.ord.IsLimit
The theorem `Cardinal.ord_isLimit` states that for any cardinal `c` (from any type universe `u_1`), if `c` is greater than or equal to `ℵ₀` (the smallest infinite cardinal), then the ordinal corresponding to `c` is a limit ordinal. A limit ordinal is an ordinal which is not zero and not a successor. This theorem essentially links the concept of cardinality with ordinals, particularly in the context of infinite sets.
More concisely: For any cardinal `c` greater than or equal to `ℵ₀`, the ordinal corresponding to `c` is a limit ordinal.
|
Cardinal.add_eq_max
theorem Cardinal.add_eq_max : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → a + b = max a b
This theorem states that if `α` is an infinite type, then the cardinality of the disjoint union of `α` and `β` is the maximum of the cardinalities of `α` and `β`. In other words, if the cardinality of `α` is at least as large as the cardinality of the smallest infinite cardinal (ℵ₀), then the cardinality of the set formed by combining `α` and `β` (denoted as `α ⊕ β`) is equal to the larger of the cardinalities of `α` and `β` (`max a b`).
More concisely: If `α` and `β` are infinite types, then the cardinality of `α ⊕ β` is `max a β`.
|
Cardinal.mk_equiv_comm
theorem Cardinal.mk_equiv_comm : ∀ {α : Type u} {β' : Type v}, Cardinal.mk (α ≃ β') = Cardinal.mk (β' ≃ α)
This theorem states that for any two types `α` and `β'`, the cardinality (or size) of the set of all bijections (one-to-one correspondences) from `α` to `β'` is equal to the cardinality of the set of all bijections from `β'` to `α`. In other words, the number of ways to uniquely map every element of `α` to an element of `β'` is the same as the number of ways to uniquely map every element of `β'` to an element of `α`. This theorem is particularly useful in cases where we know that the type `α` is infinite and we want to apply a result or lemma that assumes the type `β'` is infinite.
More concisely: The theorem asserts that for any types `α` and `β`, the number of bijections from `α` to `β` is equal to the number of bijections from `β` to `α`.
|
Cardinal.aleph0_mul_eq
theorem Cardinal.aleph0_mul_eq : ∀ {a : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → Cardinal.aleph0 * a = a
The theorem `Cardinal.aleph0_mul_eq` states that for any cardinal number `a`, if `a` is greater than or equal to `ℵ₀` (the smallest infinite cardinal), then the product of `ℵ₀` and `a` is equal to `a`. This reflects the property of infinite cardinals where multiplication does not increase the cardinality.
More concisely: For any cardinal number `a` greater than or equal to `ℵ₀`, the product of `ℵ₀` and `a` equals `a`.
|
Cardinal.mk_finsupp_lift_of_infinite
theorem Cardinal.mk_finsupp_lift_of_infinite :
∀ (α : Type u) (β : Type v) [inst : Infinite α] [inst : Zero β] [inst_1 : Nontrivial β],
Cardinal.mk (α →₀ β) = max (Cardinal.lift.{v, u} (Cardinal.mk α)) (Cardinal.lift.{u, v} (Cardinal.mk β))
The theorem `Cardinal.mk_finsupp_lift_of_infinite` states that for any two types `α` and `β`, given that `α` is infinite, `β` is a zero and `β` is nontrivial, the cardinality of the type of finite support functions from `α` to `β` is equal to the maximum of the lifted cardinalities of `α` and `β`. Here, lifting a cardinality refers to the operation that raises the universe level of the cardinality. Finite support functions from `α` to `β` are functions that only assign non-zero values to a finite number of elements in `α`.
More concisely: For infinite and nontrivial types `α` and `β`, the cardinality of finite support functions from `α` to `β` equals the maximum of the lifted cardinalities of `α` and `β`.
|
Cardinal.beth_strictMono
theorem Cardinal.beth_strictMono : StrictMono Cardinal.beth
The theorem `Cardinal.beth_strictMono` asserts that the function `Cardinal.beth` is strictly monotone. This means that for any two ordinals `a` and `b`, if `a` is less than `b`, then `beth a` is less than `beth b`. In other words, as you move to higher ordinals, the corresponding Beth numbers also increase strictly.
More concisely: For all ordinals `a` and `b` where `a` < `b`, `Cardinal.beth a` < `Cardinal.beth b`.
|
Cardinal.add_eq_left
theorem Cardinal.add_eq_left : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → b ≤ a → a + b = a
The theorem `Cardinal.add_eq_left` states that for any two cardinal numbers `a` and `b`, if the smallest infinite cardinal (`ℵ₀`) is less than or equal to `a`, and `b` is also less than or equal to `a`, then the sum of `a` and `b` is equal to `a`. In mathematical terms, this theorem asserts that for infinite cardinalities, adding a smaller cardinality to a larger one doesn't increase the larger cardinality.
More concisely: For any cardinal numbers `a` and `b` with `ℵ₀ ≤ a` and `b ≤ a`, `a + b = a`.
|
Cardinal.beth.proof_2
theorem Cardinal.beth.proof_2 : ∀ (a : Ordinal.{u_1}) (b : ↑(Set.Iio a)), ↑b ∈ Set.Iio a
This theorem, `Cardinal.beth.proof_2`, states that for any ordinal `a` and any element `b` from the set of all elements strictly less than `a` (denoted by `Set.Iio a`), the element `b` indeed belongs to the set `Set.Iio a`. In other words, if we take an element `b` from the set of values strictly less than an ordinal `a`, then `b` is confirmed to be strictly less than `a`.
More concisely: For any ordinal `a` and `b` with `b` in `Set.Iio a` (the set of elements strictly less than `a`), we have `b < a`.
|
Cardinal.power_self_eq
theorem Cardinal.power_self_eq : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → c ^ c = 2 ^ c
This theorem states that for any cardinal number `c` in a certain type universe `u_1`, if `c` is greater than or equal to aleph-zero (ℵ₀, the smallest infinite cardinal), then the cardinality of the power set of `c` is equal to the cardinality of the set of all functions from `c` to a two-element set. This is expressed in the theorem as `c ^ c = 2 ^ c`. In other words, the cardinality of all subsets of `c` is the same as the cardinality of all binary-valued functions on `c`, as long as `c` is at least as large as the cardinality of the natural numbers.
More concisely: The cardinality of the power set of a cardinal number `c` equal to or greater than aleph-zero is equivalent to the cardinality of the set of functions from `c` to a two-element set. (Or equivalently, `c ^ c = 2 ^ c`)
|
Cardinal.mul_le_max_of_aleph0_le_left
theorem Cardinal.mul_le_max_of_aleph0_le_left : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → a * b ≤ max a b := by
sorry
The theorem `Cardinal.mul_le_max_of_aleph0_le_left` states that for any two cardinal numbers `a` and `b`, if the cardinality of `a` is greater than or equal to `ℵ₀` (the smallest infinite cardinal, corresponding to the cardinality of the set of natural numbers), then the product of the cardinalities `a` and `b` is less than or equal to the maximum of `a` and `b`. In simpler terms, this theorem says that if a set has at least as many elements as the set of natural numbers, then for any other set, the size of their Cartesian product will be at most the size of the larger of the two sets.
More concisely: For any cardinal numbers `a` and `b` with `a ≥ ℵ₀`, the product `a * b` is bounded above by `max(a, b)`.
|
Cardinal.ord_card_unbounded'
theorem Cardinal.ord_card_unbounded' : Set.Unbounded (fun x x_1 => x < x_1) {b | b.card.ord = b ∧ Ordinal.omega ≤ b}
The theorem `Cardinal.ord_card_unbounded'` states that the set of infinite ordinals that are also cardinals is unbounded. In other words, for every ordinal, there exists an ordinal in this set that is greater than it. Here, an ordinal is considered infinite if it's equal or larger than `ω`, the first infinite ordinal, which is defined as the order type of the natural numbers.
More concisely: The set of infinite cardinal ordinals, which are ordinals greater than or equal to the first infinite ordinal ω, is an unbounded subset of the ordinal numbers.
|
Cardinal.mul_aleph0_eq
theorem Cardinal.mul_aleph0_eq : ∀ {a : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → a * Cardinal.aleph0 = a
The theorem `Cardinal.mul_aleph0_eq` states that for any cardinal number 'a', if aleph zero (the smallest infinite cardinal, represented by the cardinality of the set of natural numbers) is less than or equal to 'a', then the product of 'a' and aleph zero is equal to 'a'. This property mirrors the behavior of infinity in the real numbers, where multiplying infinity by any finite or infinite number still results in infinity.
More concisely: For any cardinal number 'a', if |Nat| ≤ 'a' then 'a' * |Nat| = 'a', where |Nat| denotes the cardinality of the natural numbers and |A| denotes the cardinality of set A.
|
Cardinal.beth_succ
theorem Cardinal.beth_succ : ∀ (o : Ordinal.{u_1}), Cardinal.beth (Order.succ o) = 2 ^ Cardinal.beth o
The theorem `Cardinal.beth_succ` states that for any ordinal `o`, the beth number of the successor of `o` (denoted by `Order.succ o`) is equal to 2 raised to the power of the beth number of `o` (indicated by `2 ^ Cardinal.beth o`). In mathematical terms, given an ordinal number `o`, if we denote `beth o` as the beth number associated with `o`, then the beth number of the successor of `o` is 2 to the power of `beth o`. This can be written as: `beth(succ(o)) = 2^{beth(o)}`.
More concisely: The beth number of the successor of an ordinal `o` is equal to 2 raised to the power of the beth number of `o`. In Lean notation, `Cardinal.beth_succ _ = 2 ^ Cardinal.beth`.
|
Cardinal.add_right_inj_of_lt_aleph0
theorem Cardinal.add_right_inj_of_lt_aleph0 :
∀ {α β γ : Cardinal.{u_1}}, γ < Cardinal.aleph0 → (α + γ = β + γ ↔ α = β)
This theorem states that for any three cardinal numbers `α`, `β`, and `γ`, if `γ` is less than `ℵ₀` (the smallest infinite cardinal), then the equality of `α + γ` and `β + γ` implies the equality of `α` and `β`. In other words, if `γ` is a finite cardinal number, the additive operation on the right side with `γ` is injective in the set of cardinal numbers. This mirrors the familiar property from elementary arithmetic where, if two numbers plus a same number give the same result, the two original numbers must have been equal.
More concisely: For any cardinal numbers `α`, `β`, and finite `γ`, if `α + γ = β + γ`, then `α = β`.
|
Cardinal.aleph_zero
theorem Cardinal.aleph_zero : Cardinal.aleph 0 = Cardinal.aleph0
The theorem `Cardinal.aleph_zero` states that the cardinality of the set obtained by applying the `aleph` function to 0, often denoted as ℵ₀, is equal to the smallest infinite cardinal, also denoted as ℵ₀. In other words, it asserts that the first infinite cardinal number in the `aleph` series, `Cardinal.aleph 0`, is the same as the smallest infinite cardinal number, `Cardinal.aleph0`.
More concisely: The theorem `Cardinal.aleph_zero` asserts that the cardinality of the set obtained by applying the `aleph` function to 0 equals the smallest infinite cardinal number, i.e., `Cardinal.aleph 0 = Cardinal.aleph0`.
|
Cardinal.aleph'_le
theorem Cardinal.aleph'_le : ∀ {o₁ o₂ : Ordinal.{u_1}}, Cardinal.aleph' o₁ ≤ Cardinal.aleph' o₂ ↔ o₁ ≤ o₂
The theorem `Cardinal.aleph'_le` states that for any two ordinals `o₁` and `o₂`, the cardinality of the aleph function applied to `o₁` is less than or equal to that applied to `o₂` if and only if `o₁` is less than or equal to `o₂`. In terms of set theory, it means that the order of the aleph function, which assigns cardinals to ordinals, is preserved: smaller ordinals correspond to smaller cardinals (or equivalently, smaller sizes of sets).
More concisely: The theorem `Cardinal.aleph'_le` asserts that for all ordinals `o₁ o₂`, `ℵ(o₁) ≤ ℵ(o₂)` if and only if `o₁ ≤ o₂`.
|
Cardinal.aleph_succ
theorem Cardinal.aleph_succ : ∀ {o : Ordinal.{u_1}}, Cardinal.aleph (Order.succ o) = Order.succ (Cardinal.aleph o) := by
sorry
The theorem `Cardinal.aleph_succ` states that for any ordinal `o`, the aleph of the successor of `o` is equal to the successor of the aleph of `o`. In other words, if we move to the next element in the ordinal order, the corresponding cardinal also moves to the next element. This formalizes the intuition that the aleph function and the successor operation are compatible in the sense that applying the successor operation before or after applying the aleph function yields the same result. In mathematical terms, this can be written as 𝔞(𝔬+1) = 𝔞(𝔬)+1 for all ordinals 𝔬, where 𝔞 stands for the aleph function.
More concisely: The theorem `Cardinal.aleph_succ` asserts that for all ordinals `o`, the aleph number of the successor ordinal `o+1` equals the successor of the aleph number of `o`, i.e., `aleph_o+1 = aleph_o + 1`.
|
Cardinal.mul_eq_left
theorem Cardinal.mul_eq_left : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → b ≤ a → b ≠ 0 → a * b = a
The theorem `Cardinal.mul_eq_left` states that for any two cardinal numbers `a` and `b`, if the cardinal number `a` is greater than or equal to `ℵ₀` (aleph null, the smallest infinite cardinal) and `b` is less than or equal to `a` and `b` is not zero, then the product of `a` and `b` is equal to `a`. This theorem captures an important property of cardinal arithmetic at infinity, where the multiplication of an infinite cardinal number with another cardinal that is not zero and is less than or equal to the infinite cardinal, results in the original infinite cardinal number.
More concisely: For any cardinal numbers `a` greater than or equal to `ℵ₀` and `b` less than or equal to `a` with `b` not zero, `a * b = a`.
|
Cardinal.ord_card_unbounded
theorem Cardinal.ord_card_unbounded : Set.Unbounded (fun x x_1 => x < x_1) {b | b.card.ord = b}
This theorem states that the set of ordinals that are also cardinals is unbounded. In other words, for any given ordinal, there exists an ordinal in this set that is larger than the given ordinal. Specifically, the ordinal comparison used here is the standard less than operation.
More concisely: The set of ordinals that are also cardinals is unbounded in the ordinal order.
|
Cardinal.succ_aleph0
theorem Cardinal.succ_aleph0 : Order.succ Cardinal.aleph0 = Cardinal.aleph 1
The theorem `Cardinal.succ_aleph0` states that the successor of the smallest infinite cardinal (denoted as `ℵ₀`) is equal to the `aleph` function applied to 1. In other words, the cardinality immediately following `ℵ₀` in the sequence of infinite cardinals defined by the `aleph` function, is exactly `aleph 1`. This essentially means that `aleph 1` is the first uncountable cardinal following `ℵ₀`.
More concisely: The smallest infinite cardinal `ℵ₀` has a successor equal to the first uncountable cardinal `aleph 1`.
|
Cardinal.aleph'_le_of_limit
theorem Cardinal.aleph'_le_of_limit :
∀ {o : Ordinal.{u_1}},
o.IsLimit → ∀ {c : Cardinal.{u_1}}, Cardinal.aleph' o ≤ c ↔ ∀ o' < o, Cardinal.aleph' o' ≤ c
This theorem, `Cardinal.aleph'_le_of_limit`, states that for any limit ordinal `o` and any cardinal `c`, the cardinal number `aleph' o` is less than or equal to `c` if and only if every ordinal `o'` less than `o` has its corresponding cardinal `aleph' o'` less than or equal to `c`. Essentially, it relates the ordering of limit ordinals and their corresponding cardinals in the `aleph'` sequence to the ordering of all cardinals less than a given cardinal.
More concisely: For any limit ordinal `o` and cardinal `c`, `aleph' o ≤ c` if and only if `aleph' α <= c` for all ordinals `α < o`.
|
Cardinal.mul_eq_max_of_aleph0_le_left
theorem Cardinal.mul_eq_max_of_aleph0_le_left :
∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → b ≠ 0 → a * b = max a b
The theorem `Cardinal.mul_eq_max_of_aleph0_le_left` states that for any two cardinal numbers `a` and `b` in a given type `u_1`, if `a` is greater than or equal to `ℵ₀` (aleph null, the smallest infinite cardinal) and `b` is not equal to zero, then the product of `a` and `b` is equal to the maximum of `a` and `b`. This reflects the property of infinite cardinal numbers where the multiplication of an infinite cardinal number and a non-zero cardinal number results in the larger of the two cardinal numbers.
More concisely: For any cardinal numbers `a` and `b` with `a ≥ ℵ₀` and `b ≠ 0`, we have `a * b = max {a, b}`.
|
Cardinal.pow_le
theorem Cardinal.pow_le : ∀ {κ μ : Cardinal.{u}}, Cardinal.aleph0 ≤ κ → μ < Cardinal.aleph0 → κ ^ μ ≤ κ
The theorem `Cardinal.pow_le` states that for any two cardinal numbers `κ` and `μ` in `Type u`, if `κ` is greater than or equal to `ℵ₀` (the smallest infinite cardinal number) and `μ` is less than `ℵ₀`, then `κ` raised to the power of `μ` is less than or equal to `κ`. In other words, if `κ` is at least countably infinite and `μ` is finite, then the cardinality of the set of all functions from `μ` to `κ` is at most the cardinality of `κ`.
More concisely: For any cardinal numbers `κ` greater than or equal to `ℵ₀` and finite `μ`, `κ^μ` is less than or equal to `κ`.
|
Cardinal.ord_aleph'_eq_enum_card
theorem Cardinal.ord_aleph'_eq_enum_card : Cardinal.ord ∘ Cardinal.aleph' = Ordinal.enumOrd {b | b.card.ord = b} := by
sorry
The theorem `Cardinal.ord_aleph'_eq_enum_card` states that composing the `Cardinal.ord` function with the `Cardinal.aleph'` function enumerates the ordinals that are also cardinals. Here, `Cardinal.ord` converts a cardinal number to the least ordinal with that cardinality and `Cardinal.aleph'` is a function that gives the cardinals listed by their ordinal index. The right-hand side, `Ordinal.enumOrd {b | b.card.ord = b}`, is an enumerator function that returns the least element of a set of ordinals which are cardinals. Thus, the composed function on the left-hand side and the enumerator function on the right-hand side are equivalent.
More concisely: The function `Cardinal.ord ∘ Cardinal.aleph'` is equal to the enumerator function for the ordinals that are also cardinals.
|
Cardinal.beth_zero
theorem Cardinal.beth_zero : Cardinal.beth 0 = Cardinal.aleph0
The theorem `Cardinal.beth_zero` states that the Beth number at ordinal 0 is equal to `ℵ₀`, which is the smallest infinite cardinal. In other words, `beth 0` corresponds to the cardinality of the natural numbers, according to the definition of Beth numbers in set theory.
More concisely: The theorem asserts that the Beth number at ordinal 0 equals the smallest infinite cardinal `ℵ₀`, representing the cardinality of the natural numbers.
|
Cardinal.mk_compl_of_infinite
theorem Cardinal.mk_compl_of_infinite :
∀ {α : Type u_1} [inst : Infinite α] (s : Set α),
Cardinal.mk ↑s < Cardinal.mk α → Cardinal.mk ↑sᶜ = Cardinal.mk α
This theorem, `Cardinal.mk_compl_of_infinite`, asserts that for any type `α` which is infinite, and for any set `s` of elements of this type, if the cardinality of set `s` is less than the cardinality of the type `α`, then the cardinality of the complement of set `s` (denoted `sᶜ`) is equal to the cardinality of the type `α`. In other words, for an infinite type, if a set `s` within that type has fewer elements than the type itself, the number of elements not in `s` is equal to the total number of elements in the type.
More concisely: For any infinite type `α` and set `s` with strict subset inclusion `s ��subset α`, the cardinality of the complement `sᶜ` equals that of `α`.
|
Cardinal.mul_eq_max
theorem Cardinal.mul_eq_max : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → Cardinal.aleph0 ≤ b → a * b = max a b
This theorem states that if `α` and `β` are two infinite types (meaning their cardinalities are at least ℵ₀), then the cardinality of their Cartesian product (`α × β`), is equal to the maximum of the cardinalities of `α` and `β`. In formal terms, for any two cardinals `a` and `b` such that they are both greater than or equal to ℵ₀, the product of `a` and `b` is equal to the maximum of `a` and `b`.
More concisely: If `α` and `β` are infinite types, then the cardinality of `α × β` equals the maximum of the cardinalities of `α` and `β`.
|
Cardinal.aleph'_lt
theorem Cardinal.aleph'_lt : ∀ {o₁ o₂ : Ordinal.{u_1}}, Cardinal.aleph' o₁ < Cardinal.aleph' o₂ ↔ o₁ < o₂
The theorem `Cardinal.aleph'_lt` states that for any two ordinals `o₁` and `o₂`, the Aleph function applied to `o₁` is less than the Aleph function applied to `o₂` if and only if `o₁` is less than `o₂`. In other words, this theorem guarantees that the ordinal ordering is preserved under the Aleph function.
More concisely: The Aleph function maps smaller ordinals to smaller cardinalities.
|
Ordinal.Cardinal.mk_iUnion_Ordinal_le_of_le
theorem Ordinal.Cardinal.mk_iUnion_Ordinal_le_of_le :
∀ {β : Type u_1} {o : Ordinal.{u_1}} {c : Cardinal.{u_1}},
o.card ≤ c →
Cardinal.aleph0 ≤ c →
∀ (A : Ordinal.{u_1} → Set β),
(∀ j < o, Cardinal.mk ↑(A j) ≤ c) → Cardinal.mk ↑(⋃ j, ⋃ (_ : j < o), A j) ≤ c
The theorem `Ordinal.Cardinal.mk_iUnion_Ordinal_le_of_le` establishes a bound on the cardinality of an ordinal-indexed union of sets. Specifically, given a type `β`, an ordinal `o`, and a cardinal `c`, if the cardinality of `o` is less than or equal to `c` and the cardinality of `ℵ₀` (the smallest infinite cardinal) is less than or equal to `c`, then for any function `A` mapping ordinals to sets of `β`, if the cardinality of A(j) is less than or equal to `c` for all `j` less than `o`, then the cardinality of the union of all A(j) for `j` less than `o` is also less than or equal to `c`. This theorem essentially illustrates a cardinality constraint for a union of sets indexed by ordinals.
More concisely: Given an ordinal `o`, cardinal `c` with `o` and the cardinality of `ℵ₀` less than or equal to `c`, if the cardinality of each set `A(j)` in a family indexed by `j < o` is less than or equal to `c`, then the cardinality of their union is also less than or equal to `c`.
|
Cardinal.aleph'_isNormal
theorem Cardinal.aleph'_isNormal : Ordinal.IsNormal (Cardinal.ord ∘ Cardinal.aleph')
This theorem states that the composition of the `Cardinal.ord` and `Cardinal.aleph'` functions forms a normal ordinal function. A normal ordinal function is a strictly increasing function that is also order-continuous. In this context, order-continuity means that the image of a limit ordinal under this function is the supremum of the images of all smaller ordinals. Essentially, the theorem tells us that as we move up in the ordinal index with `Cardinal.aleph'` and then map to the least ordinal of the same cardinality with `Cardinal.ord`, the resulting function preserves the order and continuity properties of normal ordinal functions.
More concisely: The composition of `Cardinal.aleph'` and `Cardinal.ord` is a normal ordinal function in Lean 4.
|
Cardinal.add_eq_self
theorem Cardinal.add_eq_self : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → c + c = c
The theorem `Cardinal.add_eq_self` states that for any cardinal number `c` (from the type of cardinal numbers `Cardinal.{u_1}`), if `c` is greater than or equal to `ℵ₀` (the smallest infinite cardinal number, represented by `Cardinal.aleph0`), then the sum of `c` and `c` is equal to `c`. In other words, if a type `α` is infinite (has cardinality at least `ℵ₀`), then the cardinality of `α ⊕ α` (the sum type of `α` and `α`, or the type of all data that either comes from `α` or from `α`) is the same as the cardinality of `α`.
More concisely: For any cardinal number `c` greater than or equal to `ℵ₀`, `c + c = c`. In other words, the cardinality of the sum type of a type of infinite cardinality is equal to its own cardinality.
|
Cardinal.mk_list_eq_mk
theorem Cardinal.mk_list_eq_mk : ∀ (α : Type u) [inst : Infinite α], Cardinal.mk (List α) = Cardinal.mk α
The theorem `Cardinal.mk_list_eq_mk` states that for any type `α` which is infinite, the cardinality of the list of `α` is equal to the cardinality of `α`. In other words, the size of the set of all lists of elements of an infinite type `α` is the same as the size of the set of elements of `α` itself. This is a reflection of a characteristic property of infinite sets in set theory: an infinite set can have the same cardinality as some of its proper subsets.
More concisely: For any infinite type `α`, the cardinality of `List α` equals the cardinality of `α`.
|
Cardinal.mk_finsupp_lift_of_infinite'
theorem Cardinal.mk_finsupp_lift_of_infinite' :
∀ (α : Type u) (β : Type v) [inst : Nonempty α] [inst : Zero β] [inst_1 : Infinite β],
Cardinal.mk (α →₀ β) = max (Cardinal.lift.{v, u} (Cardinal.mk α)) (Cardinal.lift.{u, v} (Cardinal.mk β))
The theorem `Cardinal.mk_finsupp_lift_of_infinite'` states that for any types `α` and `β`, if `α` is nonempty, `β` is a type with a zero element, and `β` is infinite, then the cardinality of the type of functions from `α` to `β` with finite support (denoted by `(α →₀ β)`) is equal to the maximum of the universe-lifted cardinalities of `α` and `β`. The universe lifting operation essentially allows comparing cardinalities of types from different universes.
More concisely: If `α` is a nonempty type, `β` is an infinite type with a zero element, then the cardinality of `(α →₀ β)` is max (|α|^U, |β|^U), where `|.|` denotes the cardinality and `^U` denotes universe lifting.
|
Cardinal.aleph0_le_aleph
theorem Cardinal.aleph0_le_aleph : ∀ (o : Ordinal.{u_1}), Cardinal.aleph0 ≤ Cardinal.aleph o
The theorem `Cardinal.aleph0_le_aleph` states that for any ordinal 'o', the cardinality of the set of natural numbers (also known as ℵ₀ or aleph-null) is less than or equal to the cardinality determined by the aleph function at 'o'. In other words, ℵ₀ is the smallest infinite cardinal and all other cardinals defined by the aleph function are at least as large.
More concisely: The theorem `Cardinal.aleph0_le_aleph` asserts that the cardinality of the natural numbers is less than or equal to the cardinality represented by the aleph function at any given ordinal.
|
Cardinal.aleph0_le_aleph'
theorem Cardinal.aleph0_le_aleph' : ∀ {o : Ordinal.{u_1}}, Cardinal.aleph0 ≤ Cardinal.aleph' o ↔ Ordinal.omega ≤ o := by
sorry
The theorem `Cardinal.aleph0_le_aleph'` states that for any ordinal number `o`, the smallest infinite cardinal number (also known as aleph-null or ℵ₀) is less than or equal to the cardinal number associated with `o` (given by the `aleph'` function) if and only if the first infinite ordinal number (often symbolized as ω) is less than or equal to `o`. In other words, it establishes a relationship between the orderings of ordinal and cardinal numbers.
More concisely: The smallest infinite cardinal number is less than or equal to the cardinality of any ordinal number `o` if and only if the first infinite ordinal number ω is less than or equal to `o`.
|
Cardinal.aleph'_succ
theorem Cardinal.aleph'_succ : ∀ {o : Ordinal.{u_1}}, Cardinal.aleph' (Order.succ o) = Order.succ (Cardinal.aleph' o)
The theorem `Cardinal.aleph'_succ` states that for any ordinal `o`, the cardinal number `aleph'` of the successor of `o` is equal to the successor of the cardinal number `aleph'` of `o`. In other words, when applied to the successor of an ordinal, the `aleph'` function commutes with the `Order.succ` function. Thus, the sequence of cardinal numbers indexed by the ordinals respects the order of the ordinals.
More concisely: The cardinal number `aleph'` of the successor ordinal is the successor of the cardinal number `aleph'` of the given ordinal.
|
Cardinal.aleph'_alephIdx
theorem Cardinal.aleph'_alephIdx : ∀ (c : Cardinal.{u_1}), Cardinal.aleph' c.alephIdx = c
The theorem `Cardinal.aleph'_alephIdx` asserts that for every cardinal number `c`, applying the function `aleph'` to the ordinal index of `c` (given by `alephIdx`) returns the cardinal `c` itself. In other words, the `aleph'` function and `alephIdx` function are inverses of each other when applied in this specific order. This means that the ordinal index of a cardinal is a unique identifier for that cardinal in the sense that no two different cardinals have the same ordinal index.
More concisely: The function `aleph'` maps the ordinal index of a cardinal `c` to `c` itself, making `alephIdx` and `aleph'` inverse functions for cardinals.
|
Cardinal.mul_eq_self
theorem Cardinal.mul_eq_self : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → c * c = c
This theorem states that if `α` is an infinite type represented by the cardinal number `c`, then the cardinality of the Cartesian product of `α` with itself (i.e., `α × α`) is the same as the cardinality of `α` itself. More formally, for any cardinal `c` such that `c` is greater than or equal to `ℵ₀` (the smallest infinite cardinal, often associated with the cardinality of the set of natural numbers), the cardinality of `c * c` (the Cartesian product of the set associated with `c` with itself) is equal to `c`.
More concisely: For any infinite cardinal `c` greater than or equal to `ℵ₀`, the cardinality of `c × c` equals `c`.
|
Cardinal.ord_aleph_eq_enum_card
theorem Cardinal.ord_aleph_eq_enum_card :
Cardinal.ord ∘ Cardinal.aleph = Ordinal.enumOrd {b | b.card.ord = b ∧ Ordinal.omega ≤ b}
The theorem `Cardinal.ord_aleph_eq_enum_card` states that the composition of the `Cardinal.ord` and `Cardinal.aleph` functions enumerates the infinite ordinals that are also cardinals. More specifically, it is equivalent to the `Ordinal.enumOrd` function applied to the set of ordinals `b` that satisfy the conditions: (1) the ordinal `b` is a cardinal (i.e., `b.card.ord = b`), and (2) `b` is greater than or equal to the first infinite ordinal, denoted as `Ordinal.omega`.
More concisely: The function `Cardinal.ord ∘ Cardinal.aleph` is equivalent to `Ordinal.enumOrd` over the set of ordinals greater than or equal to `Ordinal.omega` that are also cardinals.
|