Cardinal.derivFamily_lt_ord_lift
theorem Cardinal.derivFamily_lt_ord_lift :
∀ {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}} {c : Cardinal.{max u v}},
c.IsRegular →
Cardinal.lift.{v, u} (Cardinal.mk ι) < c →
c ≠ Cardinal.aleph0 →
(∀ (i : ι), ∀ b < c.ord, f i b < c.ord) →
∀ {a : Ordinal.{max u v}}, a < c.ord → Ordinal.derivFamily f a < c.ord
The theorem `Cardinal.derivFamily_lt_ord_lift` states that for any regular cardinal number `c` which is not equal to `ℵ₀` (the smallest infinite cardinal), if the lift of the cardinal number of a type `ι` is less than `c`, and for all function `f : ι → Ordinal → Ordinal` that for all `i` in `ι` and any ordinal `b` less than the ordinal of `c` the value `f i b` is less than the ordinal of `c`. Then for any ordinal `a` less than the ordinal of `c`, the derivative of the family `f` evaluated at `a` is also less than the ordinal of `c`. In simpler terms, this theorem is about certain properties and bounds of ordinal functions and regular cardinals.
More concisely: For any regular cardinal `c` different from `ℵ₀` and any function `f : ι → Ordinal → Ordinal` such that the lift of the cardinality of `ι` is less than `c` and `f i b` is less than the ordinal of `c` for all `i` in `ι` and ordinal `b` less than the ordinal of `c`, the derivative of `f` at any ordinal `a` less than the ordinal of `c` is also less than the ordinal of `c`.
|
Ordinal.IsNormal.cof_eq
theorem Ordinal.IsNormal.cof_eq :
∀ {f : Ordinal.{u_2} → Ordinal.{u_2}}, Ordinal.IsNormal f → ∀ {a : Ordinal.{u_2}}, a.IsLimit → (f a).cof = a.cof
This theorem states that for any normal ordinal function `f` and any limit ordinal `a`, the cofinality of `f(a)` is equal to the cofinality of `a`. Here, a normal ordinal function is a strictly increasing function that is order-continuous (the image of a limit ordinal is the supremum of the function values for lesser ordinals), a limit ordinal is an ordinal that is neither zero nor a successor, and the cofinality of an ordinal is the smallest cardinality of a subset of the ordinal which is unbounded.
More concisely: For any normal ordinal function and any limit ordinal, the cofinality of the function value at that limit ordinal equals the cofinality of the limit ordinal itself.
|
Ordinal.sup_lt_ord_lift
theorem Ordinal.sup_lt_ord_lift :
∀ {ι : Type u} {f : ι → Ordinal.{max u v}} {c : Ordinal.{max u v}},
Cardinal.lift.{v, u} (Cardinal.mk ι) < c.cof → (∀ (i : ι), f i < c) → Ordinal.sup f < c
The theorem `Ordinal.sup_lt_ord_lift` states that for any type `ι`, a function `f` from `ι` to ordinals, and an ordinal `c`, if the cardinality of the lift of `ι` is less than the cofinality of `c`, and further every ordinal obtained by applying `f` to a member of `ι` is less than `c`, then the supremum of the ordinals obtained by applying `f` to all members of `ι` is also less than `c`. In simpler terms, under given constraints on cardinality and ordinal magnitudes, this theorem gives a condition under which the supremum of a family of ordinals is less than a given ordinal.
More concisely: If `ι` is a type, `f : ι → Ordinal`, `c : Ordinal`, the cardinality of the lift of `ι` is less than the cofinality of `c`, and for all `x ∈ ι`, `f x < c`, then `sup (list (map f ι)) < c`.
|
Ordinal.aleph0_le_cof
theorem Ordinal.aleph0_le_cof : ∀ {o : Ordinal.{u_2}}, Cardinal.aleph0 ≤ o.cof ↔ o.IsLimit
This theorem, `Ordinal.aleph0_le_cof`, states that for any ordinal 'o', the smallest infinite cardinal, usually denoted as `ℵ₀` (aleph-null or aleph-zero), is less than or equal to the cofinality of 'o' if and only if 'o' is a limit ordinal. In other words, `ℵ₀` being less than or equal to the cofinality of an ordinal is both a necessary and sufficient condition for that ordinal to be a limit ordinal. In terms of set theory, the cofinality of an ordinal is the minimum cardinality of any unbounded subset of the ordinal, and a limit ordinal is an ordinal that is not zero and not a successor ordinal.
More concisely: The smallest infinite cardinal `ℵ₀` is less than or equal to the cofinality of an ordinal `o` if and only if `o` is a limit ordinal.
|
Ordinal.exists_fundamental_sequence
theorem Ordinal.exists_fundamental_sequence : ∀ (a : Ordinal.{u}), ∃ f, a.IsFundamentalSequence a.cof.ord f
The theorem `Ordinal.exists_fundamental_sequence` states that for every ordinal `a`, there exists a fundamental sequence `f` related to `a`. In other words, regardless of the ordinal we choose, we can always find a sequence that serves as the fundamental sequence for that ordinal. This fundamental sequence is associated with the cofinality of the ordinal, which is denoted by `a.cof.ord` in the theorem.
More concisely: For every ordinal `a`, there exists a fundamental sequence `f` such that the image of `f` is cofinal in `a`.
|
Cardinal.isRegular_succ
theorem Cardinal.isRegular_succ : ∀ {c : Cardinal.{u}}, Cardinal.aleph0 ≤ c → (Order.succ c).IsRegular
This theorem states that for any cardinal number `c` in any type `u`, if `c` is greater than or equal to `ℵ₀` (the smallest infinite cardinal number), then the successor of `c` (i.e., the next cardinal number after `c`), denoted by `Order.succ c`, is a regular cardinal. A regular cardinal is a cardinal that is infinite and equals its own cofinality, which is the least cardinality of a unbounded subset.
More concisely: For any cardinal number `c` in type `u` exceeding `ℵ₀`, its successor `Order.succ c` is a regular cardinal.
|
Ordinal.nfpFamily_lt_ord_lift
theorem Ordinal.nfpFamily_lt_ord_lift :
∀ {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}} {c : Ordinal.{max u v}},
Cardinal.aleph0 < c.cof →
Cardinal.lift.{v, u} (Cardinal.mk ι) < c.cof →
(∀ (i : ι), ∀ b < c, f i b < c) → ∀ {a : Ordinal.{max u v}}, a < c → Ordinal.nfpFamily f a < c
This theorem states that for any type `ι`, any function `f` from `ι` and an ordinal to an ordinal, and any ordinal `c`, if the smallest infinite cardinal (`aleph0`) is less than the cofinality of `c` and the cardinality of `ι` lifted to a higher universe is also less than the cofinality of `c`, and moreover, for every element of `ι`, the function `f` applied to that element and any ordinal less than `c` is also less than `c`, then for any ordinal `a` less than `c`, the next common fixed point of the family of functions `f` at least `a` is also less than `c`.
In simpler terms, under certain conditions on the cardinalities and the function `f`, the theorem guarantees that the "next common fixed point" of the family of functions is strictly less than a given ordinal.
More concisely: Given an ordinal `c`, a type `ι`, a function `f` from `ι` to ordinals, if `aleph0` is smaller than the cofinality of `c` and the cardinality of `ι` is also smaller than the cofinality of `c`, and for all `x ∈ ι` and `α < c`, `f(x) < c`, then for all `a < c`, there exists `x ∈ ι` such that `f^n(x) = a` for some `n`, and `f^(n+1)(x) < c`.
|
Ordinal.infinite_pigeonhole
theorem Ordinal.infinite_pigeonhole :
∀ {β α : Type u} (f : β → α),
Cardinal.aleph0 ≤ Cardinal.mk β →
Cardinal.mk α < (Cardinal.mk β).ord.cof → ∃ a, Cardinal.mk ↑(f ⁻¹' {a}) = Cardinal.mk β
This is the Infinite Pigeonhole Principle. Given two types `β` and `α`, and a function `f` from `β` to `α`, if the cardinality of `β` is greater than or equal to `ℵ₀` (the smallest infinite cardinal, equivalent to the cardinality of natural numbers), and the cardinality of `α` is less than the cofinality of the ordinal corresponding to the cardinality of `β`, then there exists an element `a` of `α` such that the cardinality of the preimage of `a` under `f` is equal to the cardinality of `β`. Essentially, if we have infinitely many "pigeons" and less "holes", at least one hole must contain infinitely many pigeons.
More concisely: If `β` is an infinite set and `α` is a set of smaller cardinality, then there exists an element `a` in `α` such that the preimage `f⁻¹{a}` under a function `f` from `β` to `α` has cardinality equal to that of `β`.
|
Ordinal.IsFundamentalSequence.cof_eq
theorem Ordinal.IsFundamentalSequence.cof_eq :
∀ {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}}, a.IsFundamentalSequence o f → a.cof.ord = o
The theorem `Ordinal.IsFundamentalSequence.cof_eq` states that for any ordinal `a` and `o`, and a function `f` from an ordinal `b` less than `o` to an ordinal, if `f` forms a fundamental sequence for `a` with length `o`, then the ordinal corresponding to the cofinality of `a` is `o`. In other words, if `f` describes a sequence that converges to `a` and has `o` as its length, which is less than or equal to the order type of the cofinality of `a`, then the smallest ordinal that has the cofinality of `a` as its cardinal is indeed `o`.
More concisely: If a function from an ordinal less than the cofinality of an ordinal `a` to `a` forms a fundamental sequence of length `o`, then the cofinality of `a` is exactly `o`.
|
Ordinal.cof_le_card
theorem Ordinal.cof_le_card : ∀ (o : Ordinal.{u_2}), o.cof ≤ o.card
The theorem `Ordinal.cof_le_card` states that for every ordinal `o`, the cofinality of `o` is less than or equal to the cardinality of `o`. In other words, the smallest cardinality of an unbounded subset of the ordinal `o` (cofinality) is always less than or equal to the cardinality of the type on which a relation with the order type defined by `o` exists (cardinality). This is applicable to all ordinals.
More concisely: The cofinality of every ordinal is less than or equal to its cardinality.
|
Ordinal.cof_lsub_def_nonempty
theorem Ordinal.cof_lsub_def_nonempty :
∀ (o : Ordinal.{u}), {a | ∃ ι f, Ordinal.lsub f = o ∧ Cardinal.mk ι = a}.Nonempty
The theorem `Ordinal.cof_lsub_def_nonempty` asserts that for any ordinal `o`, there exists a cardinal `a` such that `a` is the cardinality of some type `ι` and the least strict upper bound (`lsub`) of a function `f` mapping `ι` to ordinals is equal to `o`. In other words, the set of all such cardinals `a` is nonempty for any given ordinal `o`.
More concisely: For every ordinal `o`, there exists a cardinal `a` such that `o` is the least upper bound of the image of some function with domain of cardinality `a`.
|
Cardinal.le_range_of_union_finset_eq_top
theorem Cardinal.le_range_of_union_finset_eq_top :
∀ {α : Type u_2} {β : Type u_3} [inst : Infinite β] (f : α → Finset β),
⋃ a, ↑(f a) = ⊤ → Cardinal.mk β ≤ Cardinal.mk ↑(Set.range f)
The theorem `Cardinal.le_range_of_union_finset_eq_top` states that for any infinite type `β` and any type `α`, given a function `f` that maps elements of `α` to finite sets of `β` (`Finset β`), if the union of all those finite sets (↑(f a) where `a` is in `α`) covers the whole type `β` (equals to ⊤), then the cardinality of the collection of those finite sets (which is represented by the range of `f`) must be at least as large as the cardinality of `β`. In other words, if you can cover an infinite type with finite sets, you need at least as many sets as there are elements in the infinite type.
More concisely: If a function maps every element of an infinite type to a finite subset of another type, and the union of these subsets covers the entire second type, then the cardinality of the domain of the function is at least equal to the cardinality of the second type.
|
StrictOrder.cof_nonempty
theorem StrictOrder.cof_nonempty :
∀ {α : Type u_1} (r : α → α → Prop) [inst : IsIrrefl α r],
{c | ∃ S, Set.Unbounded r S ∧ Cardinal.mk ↑S = c}.Nonempty
The theorem `StrictOrder.cof_nonempty` asserts that for any type `α` and a relation `r` on `α` that is irreflexive (meaning for all `a` in `α`, `r a a` is not true), there exists a nonempty set consisting of cardinal numbers `c` where `c` is the cardinality of some set `S` that is unbounded with respect to the relation `r`. In other words, for every element in type `α`, there exists an element in `S` that does not have the `r` relation with the given element.
More concisely: For any irreflexive relation on a type, there exists a nonempty set of cardinalities of unbounded subsets with respect to that relation.
|
Order.cof_nonempty
theorem Order.cof_nonempty :
∀ {α : Type u_1} (r : α → α → Prop) [inst : IsRefl α r],
{c | ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ Cardinal.mk ↑S = c}.Nonempty
The theorem `Order.cof_nonempty` asserts that for any type `α` and a relation `r` on `α` that is reflexive (i.e., for all `a` in `α`, `r a a` holds), there exists a nonempty set `S` with a certain property: for each element `a` of `α`, there is an element `b` in `S` such that `r a b` holds, and the cardinality of `S` is equal to some cardinal number `c`. In other words, in the context of order theory, this theorem guarantees the non-emptiness of the set of cofinalities of a reflexive relation.
More concisely: For any reflexive relation `r` on a type `α`, there exists a nonempty set `S` of elements in `α` such that each element has a related element in `S`, and the cardinality of `S` is some fixed cardinal number.
|
Ordinal.unbounded_of_unbounded_sUnion
theorem Ordinal.unbounded_of_unbounded_sUnion :
∀ {α : Type u_1} (r : α → α → Prop) [wo : IsWellOrder α r] {s : Set (Set α)},
Set.Unbounded r s.sUnion → Cardinal.mk ↑s < StrictOrder.cof r → ∃ x ∈ s, Set.Unbounded r x
The theorem `Ordinal.unbounded_of_unbounded_sUnion` states the following: For any type `α`, any relation `r` on `α` that forms a well-ordering, and any set `s` of subsets of `α`, if the union of the sets in `s` is unbounded with respect to `r` and the cardinality of `s` is less than the cofinality of `r`, then there exists a subset `x` in `s` that is also unbounded with respect to `r`.
In other words, if we have a well-ordered set and a collection of subsets whose union is unbounded, and if the number of these subsets is smaller than the smallest size of any unbounded subset, then at least one of these subsets must itself be unbounded.
More concisely: If `α` is a type with a well-ordering `r`, `s` is a set of subsets of `α` with cardinality less than the cofinality of `r`, and the union of `s` is unbounded with respect to `r`, then there exists an `x` in some set in `s` that is also unbounded with respect to `r`.
|
Cardinal.exists_infinite_fiber
theorem Cardinal.exists_infinite_fiber :
∀ {β α : Type u} (f : β → α), Cardinal.mk α < Cardinal.mk β → Infinite α → ∃ a, Infinite ↑(f ⁻¹' {a})
This theorem states that for any two types `β` and `α`, given a function `f` from `β` to `α`, if the cardinality (or size) of `α` is strictly lesser but infinite compared to the cardinality of `β`, then there exists an element `a` in `α` such that the preimage of `a` under `f` (denoted by `f ⁻¹' {a}`) is infinite. In other words, there are infinitely many elements in `β` that map to the same element `a` in `α` under the function `f`.
More concisely: For any function `f` from an infinite, but strictly smaller cardinality type `β` to a type `α`, there exists an element `a` in `α` such that the preimage `f⁻¹{a}` is infinite.
|
Ordinal.cof_zero
theorem Ordinal.cof_zero : Ordinal.cof 0 = 0
The theorem `Ordinal.cof_zero` states that the cofinality of the ordinal 0 is 0. In other words, the smallest cardinality of a subset of the ordinal 0 which is unbounded, where an unbounded subset is one for which every element of the ordinal has an equal or larger element in the subset, is 0. This aligns with the general definition of cofinality, considering the special case where the ordinal is 0.
More concisely: The cofinality of the ordinal 0 is 0.
|
Ordinal.cof_succ
theorem Ordinal.cof_succ : ∀ (o : Ordinal.{u_2}), (Order.succ o).cof = 1
This theorem states that for every ordinal `o`, the cofinality of the successor of `o` is `1`. In other words, the smallest cardinality of a subset `S` of the successor ordinal such that every element of the successor ordinal is less than or equal to some element of `S`, is `1`. This theorem implies that the successor of any ordinal has a minimal unbounded subset of cardinality `1`.
More concisely: For every ordinal `o`, the cofinality of `o'` (the successor of `o`) equals 1.
|
Cardinal.infinite_pigeonhole_card_lt
theorem Cardinal.infinite_pigeonhole_card_lt :
∀ {β α : Type u} (f : β → α),
Cardinal.mk α < Cardinal.mk β → Cardinal.aleph0 ≤ Cardinal.mk α → ∃ a, Cardinal.mk α < Cardinal.mk ↑(f ⁻¹' {a})
The theorem `Cardinal.infinite_pigeonhole_card_lt` states that for any two types `α` and `β` and any function `f` from `β` to `α`, if the cardinality of `α` is less than the cardinality of `β` and the cardinality of `α` is at least ℵ₀ (the smallest infinite cardinal, which is the cardinality of the natural numbers), then there exists an element `a` in `α` such that the cardinality of the preimage of `a` under `f` (the set of all elements in `β` that `f` maps to `a`) is strictly greater than the cardinality of `α`. This is a version of the infinite pigeonhole principle, which in this case states that if you have 'more' holes than pigeons and infinitely many pigeons, then there must be a hole with 'more' pigeons than there are total holes.
More concisely: For any function from a type of strictly larger cardinality to a countable type, there exists an image element with a strictly larger preimage cardinality.
|
Ordinal.blsub_lt_ord_lift
theorem Ordinal.blsub_lt_ord_lift :
∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {c : Ordinal.{max u v}},
Cardinal.lift.{v, u} o.card < c.cof → (∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) → o.blsub f < c
This theorem states that for any ordinal `o`, any function `f` mapping each ordinal less than `o` to an ordinal (possibly in a larger universe), and any ordinal `c`, if the cardinality of `o` (when lifted to the universe of `c`) is less than the cofinality of `c`, and if `f` maps every ordinal less than `o` to an ordinal less than `c`, then the least strict upper bound of the family of ordinals given by `f` (as described by the `blsub` operation) is less than `c`. In essence, this theorem is about comparing the size of a certain construct, `blsub`, to another ordinal `c` under specific conditions.
More concisely: For any ordinal `o`, function `f` mapping `o` to ordinals in a larger universe, and ordinal `c` with `o` having strictly smaller cardinality when lifted to `c` and all `f(x) < c`, the least strict upper bound of `f` (`blsub f`) is strictly less than `c`.
|
Ordinal.cof_blsub_le_lift
theorem Ordinal.cof_blsub_le_lift :
∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}),
(o.blsub f).cof ≤ Cardinal.lift.{v, u} o.card
The theorem `Ordinal.cof_blsub_le_lift` states that for any ordinal `o` and a function `f` from an ordinal less than `o` to another ordinal, the cofinality of the least upper bound of the family of ordinals indexed by the set of ordinals less than `o` (`Ordinal.blsub o f`) is less than or equal to the lift of the cardinality of `o`. Here, the cofinality of an ordinal is the smallest cardinality of a subset that is unbounded in the ordinal, the lift operation on cardinals changes the universe level of the cardinal, and the cardinality of an ordinal is the cardinality of any type on which a relation with that order type is defined.
More concisely: The cofinality of the least upper bound of a family of ordinals less than `o` indexed by the function `f` is less than or equal to the lift of the cardinality of `o`.
|
Ordinal.cof_eq_sInf_lsub
theorem Ordinal.cof_eq_sInf_lsub :
∀ (o : Ordinal.{u}), o.cof = sInf {a | ∃ ι f, Ordinal.lsub f = o ∧ Cardinal.mk ι = a}
This theorem states that for any ordinal `o`, the cofinality of `o` is equal to the infimum of the set of all cardinals `a` such that there exists an index set `ι` and a function `f` from `ι` to the ordinal numbers, where `o` is the least strict upper bound of the function `f` and `a` is the cardinality of the index set `ι`. In simpler terms, the theorem relates the cofinality of an ordinal to the least upper bound of a family of ordinals and the cardinality of the index set over which this family is defined.
More concisely: The cofinality of an ordinal `o` is the smallest cardinality of an index set `ι` and the cardinality of `ι` such that there exists a function `f: ι -> On` with `o` as the least upper bound of `range(f)`.
|
Cardinal.IsRegular.cof_eq
theorem Cardinal.IsRegular.cof_eq : ∀ {c : Cardinal.{u_2}}, c.IsRegular → c.ord.cof = c
This theorem states that for any regular cardinal 'c', the cofinality of the ordinal corresponding to 'c' is equal to 'c' itself. In the context of set theory, a regular cardinal is an infinite cardinal number that cannot be represented as a smaller set of smaller cardinals, i.e., it equals its own cofinality. The cofinality of an ordinal is the smallest cardinal of a subset of the ordinal which is unbounded. The ordinal corresponding to a cardinal 'c' is essentially the least ordinal whose cardinal is 'c'. This theorem formally establishes the property of regular cardinals in Lean 4.
More concisely: For any regular cardinal 'c', the ordinal of cardinality 'c' has cofinality 'c'.
|
Ordinal.unbounded_of_unbounded_iUnion
theorem Ordinal.unbounded_of_unbounded_iUnion :
∀ {α β : Type u} (r : α → α → Prop) [wo : IsWellOrder α r] (s : β → Set α),
Set.Unbounded r (⋃ x, s x) → Cardinal.mk β < StrictOrder.cof r → ∃ x, Set.Unbounded r (s x)
This theorem, named `Ordinal.unbounded_of_unbounded_iUnion`, states that for any two types `α` and `β`, and a relation `r` on `α` that is a well order, if we have a mapping `s` from `β` to the set of `α`, such that the union of the sets `s x` (for every `x` in `β`) is unbounded with respect to `r` and the cardinal number of `β` is strictly less than the cofinality of `r`, then there exists at least one `x` in `β` for which the set `s x` is unbounded with respect to `r`.
In simpler words, if we have a collection of sets that is unbounded and the size of the collection itself is less than the smallest size of an unbounded set, then there must be at least one set within the collection that is unbounded.
More concisely: If `α` and `β` are types, `r` is a well order on `α`, `s : β → α`, and the union of `s x` is unbounded with respect to `r` and the cardinality of `β` is strictly less than the cofinality of `r`, then there exists an `x` in `β` such that `s x` is unbounded with respect to `r`.
|
Ordinal.infinite_pigeonhole_card
theorem Ordinal.infinite_pigeonhole_card :
∀ {β α : Type u} (f : β → α),
∀ θ ≤ Cardinal.mk β, Cardinal.aleph0 ≤ θ → Cardinal.mk α < θ.ord.cof → ∃ a, θ ≤ Cardinal.mk ↑(f ⁻¹' {a})
This theorem is a version of the infinite pigeonhole principle for cardinals. Suppose we have two types `β` and `α` and a function `f` from `β` to `α`. If we have a cardinal number `θ` less than or equal to the cardinality of `β` and greater than or equal to the smallest infinite cardinal (`aleph0`), and if the cofinality of the ordinal of `θ` is greater than the cardinality of `α`, then there is an element `a` in `α` such that the cardinality of the preimage of `a` under `f` is at least `θ`. In other words, for sufficiently large `θ`, there are at least `θ` elements in `β` mapped to the same element in `α` by `f`.
More concisely: Given types `β` and `α`, a function `f` from `β` to `α`, and a cardinal number `θ` greater than `aleph0` with cofinality greater than the cardinality of `α`, there exists an element `a` in `α` such that the preimage of `a` under `f` has cardinality at least `θ`.
|
Ordinal.lsub_lt_ord_lift
theorem Ordinal.lsub_lt_ord_lift :
∀ {ι : Type u} {f : ι → Ordinal.{max u v}} {c : Ordinal.{max u v}},
Cardinal.lift.{v, u} (Cardinal.mk ι) < c.cof → (∀ (i : ι), f i < c) → Ordinal.lsub f < c
The theorem `Ordinal.lsub_lt_ord_lift` asserts that for any type `ι`, a function `f` from `ι` to an ordinal `c` (both in the same or different universes), if the cardinality of `ι` after lifting to the universe of `c` is strictly less than the cofinality of `c`, and for any element `i` of `ι`, `f(i)` is less than `c`, then the least strict upper bound of the family `f` (denoted by `Ordinal.lsub f`) is strictly less than `c`. In simple words, if the associated set for `c` is "large enough" (as measured by its cofinality) and all elements of the set mapped by `f` are less than `c`, then the least upper bound of this function is also less than `c`.
More concisely: If `ι` is a type, `c` is an ordinal, `f : ι → c`, `ℵ(ι) < cofinality(c)`, and for all `i ∈ ι`, `f(i) < c`, then `Ordinal.lsub f < c`.
|
Ordinal.cof_lsub_le_lift
theorem Ordinal.cof_lsub_le_lift :
∀ {ι : Type u} (f : ι → Ordinal.{max u v}), (Ordinal.lsub f).cof ≤ Cardinal.lift.{v, u} (Cardinal.mk ι)
The theorem `Ordinal.cof_lsub_le_lift` states that for any type `ι` and any function `f` from `ι` to the set of ordinals, the cofinality of the least strict upper bound of the image of `f` is less than or equal to the cardinality of `ι` lifted to the maximum of `v` and `u`. In simpler terms, it establishes a bound on the smallest size of an unbounded subset (cofinality) of the least upper bound of a set of ordinals, in terms of the size of the set from which the ordinals are drawn.
More concisely: The cofinality of the least upper bound of a function from a type `ι` to ordinals is less than or equal to the cardinality of `ι` lifted to the maximum of the cofinalities of `v` and `u`.
|