Revision #1446 → #1773 · back to history
modifiedComparability of well-ordered sets818a2eeaca6f
| Field | From #1446 | To #1773 |
|---|
| note | For any two well-orders, one is an initial segment of the other (and isomorphism is the equality case). | `InitialSeg.total` shows for any two well-orders, one is an initial segment of the other. |
modifiedWell-orderdd12f8631460
| Field | From #1446 | To #1773 |
|---|
| note | `IsWellOrder` is the typeclass for a relation that is trichotomous, transitive and well-founded. | `IsWellOrder` is the typeclass for a trichotomous, transitive, well-founded relation. |
modifiedOrdinals as isomorphism class representativesfdc305d374d4
| Field | From #1446 | To #1773 |
|---|
| note | `Ordinal.type` maps a well-order to its order-isomorphism class, the ordinal. | `Ordinal.type` maps a well-order to its order-isomorphism class. |
modifiedWell-ordered set (ZF)11ce9cc4fbda
| Field | From #1446 | To #1773 |
|---|
| note | `IsWellOrder` captures a total order in which every nonempty subset has a least element. | `IsWellOrder` captures a total order whose every nonempty subset has a least element. |
modifiedOrder isomorphisma4b63fb79c01
| Field | From #1446 | To #1773 |
|---|
| note | `OrderIso` (and `RelIso`) is an order-preserving bijection between ordered sets. | `OrderIso` is the order-preserving bijection between ordered types. |
modifiedOrder-isomorphism is an equivalence relation9e2ffed0c8ac
| Field | From #1446 | To #1773 |
|---|
| note | The `Setoid` instance `Ordinal.isEquivalent` is precisely order-isomorphism as an equivalence relation on well-orders. | `Ordinal.isEquivalent` is the `Setoid` of order-isomorphism on well-orders. |
modifiedMostowski collapse lemma30ef18707a68
| Field | From #1446 | To #1773 |
|---|
| note | Mathlib has the order-embedding collapse into an initial segment, but not the general set-theoretic Mostowski transitive collapse by name. | Mathlib has the order-embedding collapse into an initial segment but not the general set-theoretic Mostowski transitive collapse by name. |
modifiedFinite von Neumann ordinals9e9877e6d942
| Field | From #1446 | To #1773 |
|---|
| note | `ZFSet.omega` is the set of finite von Neumann ordinals, built from `∅` (omega_zero) and `insert x x` (omega_succ). | `ZFSet.omega` is the set of finite von Neumann ordinals built from `∅` and `insert x x`. |
modifiedOmega as smallest inductive setd15e245a266d
| Field | From #1446 | To #1773 |
|---|
| note | `ZFSet.omega` is defined directly from ℕ and shown inductive (omega_zero/omega_succ), but not characterized as the smallest inductive set. | `ZFSet.omega` is constructed directly from ℕ; it is not characterized as the smallest inductive set in Mathlib. |
modifiedCharacterization of the order relationa8e045300231
| Field | From #1446 | To #1773 |
|---|
| note | For ordinals, `x ⊆ y ↔ x = y ∨ x ∈ y`, i.e. `≤` is `⊆` and `<` is `∈`. | For ordinals, `x ⊆ y ↔ x = y ∨ x ∈ y`, exactly the alternative characterization. |
modifiedOrdinals are totally ordered and well-ordered15ce227a47bc
| Field | From #1446 | To #1773 |
|---|
| note | `Ordinal` has a `LinearOrder` instance and `Ordinal.lt_wf`/`WellFoundedLT` makes it a well-order. | `Ordinal` has a `LinearOrder` instance and `Ordinal.lt_wf` provides well-foundedness. |
modifiedUnion of a set of ordinals is an ordinalc19ac3f1aac1
| Field | From #1446 | To #1773 |
|---|
| note | Any (small) set of ordinals is bounded above, so its `sSup`/`iSup` (the union) is again an ordinal. | Any small set of ordinals is bounded above, so its `sSup` is again an ordinal. |
modifiedExistence of a greater ordinaldfcd78d6b99a
| Field | From #1446 | To #1773 |
|---|
| note | Every ordinal is below its successor, so the successor of the supremum of a set exceeds all its members. | Every ordinal is below its successor, so the successor of the supremum exceeds all members. |
modifiedBurali-Forti paradox99a3ceffdbd7
| Field | From #1446 | To #1773 |
|---|
| note | `not_small_ordinal` is the formal content of Burali-Forti: `Ordinal` is not a small type (a proper class). | `not_small_ordinal` is the formal content of Burali-Forti: `Ordinal` is a proper class. |
modifiedThree types of ordinals8057ae79e4da
| Field | From #1446 | To #1773 |
|---|
| note | Every ordinal is zero, a successor, or a (successor) limit. | Every ordinal is zero, a successor, or a limit. |
modifiedZero ordinal0865bbac54ac
| Field | From #1446 | To #1773 |
|---|
| mathlib.decl | Ordinal.zero_le | Ordinal.bot_eq_zero |
| note | `0 : Ordinal` exists and `Ordinal.zero_le` shows it is the least ordinal. | `Ordinal.bot_eq_zero` together with the `OrderBot` instance gives that `0` is the least ordinal. |
modifiedSuccessor ordinal9f2ed9575b80
| Field | From #1446 | To #1773 |
|---|
| note | Ordinals have a `SuccOrder` instance; `Order.succ o` is the successor ordinal (`= o + 1`). | Ordinals have a `SuccOrder` instance; `Order.succ o` is the successor ordinal. |
modifiedLimit ordinal5d7b630bb1a4
| Field | From #1446 | To #1773 |
|---|
| note | `Order.IsSuccLimit` (used for ordinals) is the limit-ordinal predicate. | `Order.IsSuccLimit` is the limit-ordinal predicate Mathlib uses for ordinals. |
modifiedLimit ordinal is supremum of smaller ordinals71f12ccbfa1c
| Field | From #1446 | To #1773 |
|---|
| mathlib.decl | IsSuccPrelimit.sSup_Iio | Order.IsSuccPrelimit.sSup_Iio |
| mathlib.module | Mathlib.SetTheory.Ordinal.Family | Mathlib.Order.SuccPred.CompleteLinearOrder |
modifiedOmega is the least limit ordinal523b06a7a331
| Field | From #1446 | To #1773 |
|---|
| note | `omega0_le_of_isSuccLimit` shows ω ≤ any limit ordinal, i.e. ω is the least limit. | `omega0_le_of_isSuccLimit` shows ω ≤ any limit ordinal, so ω is the least limit. |
modifiedNo infinite descending chainsdc75ac5c675d
| Field | From #1446 | To #1773 |
|---|
| note | `Ordinal.lt_wf` (the `WellFoundedLT` instance) means there are no infinite descending chains. | `Ordinal.lt_wf` means there are no infinite descending chains of ordinals. |
modifiedTermination of procedures9c2ee59dcd92
| Field | From #1446 | To #1773 |
|---|
| note | This is a methodological remark; Mathlib uses well-founded recursion but no theorem states this application. | This is a methodological remark; Mathlib uses well-founded recursion but does not state this as a theorem. |
modifiedTransfinite sequence7ba67198e28b
| Field | From #1446 | To #1773 |
|---|
| note | Ordinal-indexed sequences are represented as functions/bounded families, with no dedicated 'transfinite sequence' type. | Ordinal-indexed sequences appear as bounded families; there is no dedicated 'transfinite sequence' type. |
modifiedClass-indexed sequence is a proper class94408091ce67
| Field | From #1446 | To #1773 |
|---|
| note | Mathlib does not reify proper classes, so a sequence indexed by all ordinals being a proper class is not stated. | Mathlib does not reify proper classes, so this is not formalized. |
modifiedLimit of an increasing transfinite sequenceeff11e7fe830
| Field | From #1446 | To #1773 |
|---|
| note | The supremum `iSup`/`sSup` of an ordinal family is its least upper bound (the limit). | The supremum `iSup` of an ordinal family is its least upper bound (the limit). |
modifiedContinuous transfinite sequence434b89809709
| Field | From #1446 | To #1773 |
|---|
| note | Continuity (preserving suprema at limits) is bundled into `Order.IsNormal` rather than defined separately. | Continuity is bundled into `Order.IsNormal` rather than defined as a standalone predicate. |
modifiedNormal sequencecb02d9c21a25
| Field | From #1446 | To #1773 |
|---|
| note | `Order.IsNormal` means strictly monotone and continuous (sup-preserving at limits). | `Order.IsNormal` is exactly: strictly monotone and continuous (sup-preserving at limits). |
modifiedExistence and uniqueness of recursive functionse2d52f0da2fa
| Field | From #1446 | To #1773 |
|---|
| note | `limitRecOn` plus its `_zero/_succ/_limit` computation rules give existence and (definitional) uniqueness. | `limitRecOn` with its computation rules gives existence and definitional uniqueness. |
modifiedAdditively indecomposable ordinal299f6c2bbbf8
| Field | From #1446 | To #1773 |
|---|
| note | `IsPrincipal (·+·) a ↔ ∀ b<a, ∀ c<a, b+c ≠ a` is exactly additive indecomposability. | `IsPrincipal (·+·) a` is exactly additive indecomposability. |
modifiedEpsilon numbers138e4375267e
| Field | From #1446 | To #1773 |
|---|
| note | `Ordinal.epsilon = veblen 1` enumerates the epsilon numbers (fixed points of ω^·). | `Ordinal.epsilon` enumerates the epsilon numbers (fixed points of `ω^·`). |
modifiedNatural operations on ordinalsbc97163ca742
| Field | From #1446 | To #1773 |
|---|
| note | Natural (Hessenberg) sum/product of ordinals is not present in Mathlib. | Natural (Hessenberg) sum/product of ordinals is not in Mathlib. |
modifiedAxiom of choice and well-ordering5ba0d0b375cb
| Field | From #1446 | To #1773 |
|---|
| note | The well-ordering theorem is proved from Lean's choice axiom, but the equivalence AC ⇔ well-ordering is not formalized. | The well-ordering theorem is derived from Lean's choice, but the AC ⇔ well-ordering equivalence is not formalized. |
modifiedInfinite initial ordinals are limit ordinalsf28135ad3663
| Field | From #1446 | To #1773 |
|---|
| mathlib.decl | Ordinal.isSuccLimit_ord | Cardinal.isSuccLimit_ord |
| note | `isSuccLimit_ord` shows `ord c` is a limit ordinal whenever `ℵ₀ ≤ c`. | `Cardinal.isSuccLimit_ord` shows `c.ord` is a limit ordinal whenever `ℵ₀ ≤ c`. |
modifiedSmallest uncountable ordinal22dfbf0e27d4
| Field | From #1446 | To #1773 |
|---|
| note | `ω₁ = Ordinal.omega 1` is defined and documented as the first uncountable ordinal. | `ω₁ = Ordinal.omega 1` is documented as the first uncountable ordinal. |
modifiedCofinalityb9adb51adf7a
| Field | From #1446 | To #1773 |
|---|
| note | `Ordinal.cof` is the least cardinality of a cofinal subset (cardinal-valued cofinality). | `Ordinal.cof` is the cardinal cofinality of an ordinal. |
modifiedCountable limit ordinals have cofinality omegad549a1d0b12d
| Field | From #1446 | To #1773 |
|---|
| note | A limit ordinal below ω₁ has cofinality ℵ₀. | A countable limit ordinal has cofinality ℵ₀. |
modifiedRegular ordinald4854f5f2f15
| Field | From #1446 | To #1773 |
|---|
| note | Mathlib defines regular cardinals (`Cardinal.IsRegular`); there is no standalone 'regular ordinal' predicate. | Mathlib defines regular cardinals; there is no standalone 'regular ordinal' predicate. |
modifiedUnbounded (cofinal) subsetd40864263e29
| Field | From #1446 | To #1773 |
|---|
| note | `IsCofinal s : ∀ x, ∃ y ∈ s, x ≤ y` is the unbounded/cofinal subset notion. | `IsCofinal s` is the unbounded/cofinal subset notion. |
modifiedLimit pointfd67df621bc0
| Field | From #1446 | To #1773 |
|---|
| note | `Ordinal.IsAcc o S` is `AccPt o (𝓟 S)`, i.e. `o` is a limit point of `S`. | `Ordinal.IsAcc o S` says `o` is a limit point of `S`. |
modifiedClub set3d51e154cd3d
| Field | From #1446 | To #1773 |
|---|
| note | There is no club (closed-unbounded) predicate in Mathlib (only the separate closed and unbounded notions). | There is no club (closed-unbounded) predicate in Mathlib. |
modifiedRange of a normal function is club7d2e18082216
| Field | From #1446 | To #1773 |
|---|
| note | Mathlib links normal enumerations with closed sets, but does not state the range of a normal function is a club. | Mathlib links normal enumerations with closed sets but does not state the range of a normal function is a club. |
modifiedIntersection of club sets is clubc744b796f7fe
| Field | From #1446 | To #1773 |
|---|
| note | Not formalized; a Mathlib TODO note even flags this as future work. | Not formalized in Mathlib. |
modifiedUnbounded and closed classes of ordinals50205e53c861
| Field | From #1446 | To #1773 |
|---|
| mathlib.decl | Unbounded | Set.Unbounded |
| note | `Unbounded (·<·)` (with order-topology closedness) covers subsets of `Ordinal`; dedicated proper-class versions are not formalized. | `Set.Unbounded` covers subsets of `Ordinal`; dedicated proper-class versions are not formalized. |
modifiedEpsilon-zerod18bf0236138
| Field | From #1446 | To #1773 |
|---|
| note | `ε₀` is defined (`ε_ 0`) and characterized as the least fixed point of `ω^·`. | `ε₀` is characterized as the least fixed point of `ω^·`. |
modifiedCantor's derived set theoremsab6a90570b0f
| Field | From #1446 | To #1773 |
|---|
| note | Mathlib has the Cantor–Bendixson theorem (closed = perfect ∪ countable) but not the transfinite derived-set/rank iteration. | Mathlib has Cantor–Bendixson but not the transfinite derived-set rank iteration. |
modifiedFirst and second number classesee5fdfe2800a
| Field | From #1446 | To #1773 |
|---|
| note | Cantor's 'number classes' terminology/objects are not formalized in Mathlib. | Cantor's 'number classes' terminology is not formalized in Mathlib. |
modifiedCardinality of the second number classa7a517d3ac46
| Field | From #1446 | To #1773 |
|---|
| note | `card_omega` gives `card ω₁ = ℵ₁`, the cardinality of the countable ordinals, though 'number class' is not named. | `card_omega` gives `card ω₁ = ℵ₁`, the cardinality of the countable ordinals. |
modifiedNumber classes correspond to aleph numbers39cfc64ff526
| Field | From #1446 | To #1773 |
|---|
| note | The aleph/initial-ordinal correspondence is formalized via `Cardinal.aleph`/`Ordinal.omega`, but not phrased as number classes. | The aleph/initial-ordinal correspondence is formalized via `Cardinal.aleph`/`Ordinal.omega`. |
addedAxiom of choice implies every set is well-orderabled87e0d15f8ee
addedPerfect set is uncountable184d9f6ded61
addedCantor–Bendixson theorem90ccb010e795