Revision #3198 → #3709 · back to history
modifiedTransitivity tacitly required3603bafd4842
| Field | From #3198 | To #3709 |
|---|
| note | This is a meta-convention, not a theorem; though Mathlib's `IsWellOrder` does derive an `IsTrans` instance automatically. | Meta-convention rather than a theorem; `IsWellOrder` derives an `IsTrans` instance automatically. |
modifiedWell-order27332daabaed
| Field | From #3198 | To #3709 |
|---|
| note | `IsWellOrder` is a relation that is well-founded and trichotomous (hence a well-founded linear order). | `IsWellOrder` bundles trichotomy plus well-foundedness, giving a well-founded strict total order. |
modifiedWell-ordered setbc08be407bf2
| Field | From #3198 | To #3709 |
|---|
| note | `WellOrder` bundles a type, a relation, and a proof that the relation is an `IsWellOrder`. | `WellOrder` packages a type, a relation, and an `IsWellOrder` proof. |
modifiedExistence of least elementdcacadb5c169
| Field | From #3198 | To #3709 |
|---|
| note | `WellFounded.has_min` gives a minimal element of any nonempty set under a well-founded relation, generalizing the well-order case. | `WellFounded.has_min` produces a minimal element in every nonempty set under a well-founded relation. |
modifiedUnique successor69ad49a0b289
| Field | From #3198 | To #3709 |
|---|
| note | A well-order is made into a `SuccOrder` whose `Order.succ` is the next element (the min of strictly larger elements). | A well-order is endowed with a `SuccOrder` whose `Order.succ` is the next element. |
modifiedLeast upper bound of bounded subsets0acf7c651b3b
| Field | From #3198 | To #3709 |
|---|
| note | Any well-founded linear order with a bottom is conditionally complete, so every bounded-above set has a least upper bound. | Any well-founded linear order with a bottom is conditionally complete, so bounded-above sets have a supremum. |
modifiedNon-strict yields strict well ordering1259397265bc
| Field | From #3198 | To #3709 |
|---|
| note | From a `LinearOrder` with `WellFoundedLT` Mathlib derives `IsWellOrder α (· < ·)`, i.e. the strict version is a strict well order. | From a `LinearOrder` with `WellFoundedLT` Mathlib derives `IsWellOrder α (· < ·)`, the strict version. |
modifiedStrict well ordering characterization85306096528e
| Field | From #3198 | To #3709 |
|---|
| note | `IsWellOrder` is defined as well-founded + trichotomous and carries an `IsStrictTotalOrder` instance, which is exactly a well-founded strict total order. | `IsWellOrder` is defined as well-founded + trichotomous, i.e. a well-founded strict total order. |
modifiedOrder type ordinal isomorphism9a2c2f6e3fa2
| Field | From #3198 | To #3709 |
|---|
| note | `Ordinal.type` assigns the order type, and `Ordinal.type_eq` shows two well orders are order-isomorphic iff they have the same ordinal. | `Ordinal.type` gives the order type, and `Ordinal.type_eq` says two well orders share it iff order-isomorphic. |
modifiedWell-ordering theorem2294662781f0
| Field | From #3198 | To #3709 |
|---|
| note | `exists_wellFoundedLT` (Zermelo's theorem) gives every type a well-order using choice; the explicit equivalence to AC is not separately formalized. | `exists_wellFoundedLT` (Zermelo) endows any type with a well-order via choice; the equivalence to AC is not separately isolated. |
modifiedTransfinite induction applicability978d8ec139e5
| Field | From #3198 | To #3709 |
|---|
| note | `WellFoundedLT.induction` (and `Ordinal.inductionOn`) provide transfinite/well-founded induction. | `WellFoundedLT.induction` provides well-founded/transfinite induction on any well-order. |
modifiedWell-ordering principle81760a927823
| Field | From #3198 | To #3709 |
|---|
| note | `type_nat_lt` (typeLT ℕ = ω) records that ℕ under `<` is a well order, the content of the well-ordering principle. | `type_nat_lt` records that ℕ under `<` is a well order (type ω). |
modifiedStandard order on naturals38ba5e38ab7e
| Field | From #3198 | To #3709 |
|---|
| note | `type_nat_lt` states ℕ's standard order is a well order of type ω (ℕ also has a `WellFoundedLT` instance). | `type_nat_lt` states ℕ's standard order is a well order of type ω (ℕ has a `WellFoundedLT` instance). |
modifiedEvens-before-odds order (type ω+ω)874ef6a98e7a
| Field | From #3198 | To #3709 |
|---|
| note | This specific reordering of ℕ giving order type ω+ω is not formalized. | This specific reordering of ℕ of type ω+ω is not formalized. |
modifiedStandard order on integers not a well orderf2b81a11caa6
| Field | From #3198 | To #3709 |
|---|
| note | There is no explicit statement that ℤ is not well-ordered (ℤ simply has no `WellFoundedLT` instance and is `NoMinOrder`). | No explicit statement that ℤ is not well-ordered by ≤ was found. |
modifiedWell order R of integers (type ω+ω)53d97532ad1a
| Field | From #3198 | To #3709 |
|---|
| note | This explicit well order of ℤ of type ω+ω is not formalized. | The specific ω+ω well-ordering of ℤ is not formalized. |
modifiedAlternate well order of integers (type ω)893b040946f9
| Field | From #3198 | To #3709 |
|---|
| note | This alternate well order of ℤ of type ω is not formalized. | This alternate ω-type well ordering of ℤ is not formalized. |
modifiedZFC implies a well order of the reals15c0ecf304b6
| Field | From #3198 | To #3709 |
|---|
| note | Instantiating `exists_wellFoundedLT` at ℝ yields a well order of the reals. | Instantiating `exists_wellFoundedLT` at ℝ gives a well order of the reals. |
modifiedSierpiński: ZF+GCH implies AC60f83621ee90
| Field | From #3198 | To #3709 |
|---|
| note | Sierpiński's theorem that GCH implies AC over ZF is not formalized in Mathlib. | Sierpiński's ZF+GCH ⇒ AC theorem is not formalized in Mathlib. |
modifiedZFC+V=L gives definable well orderf8355b03f4e4
| Field | From #3198 | To #3709 |
|---|
| note | V=L and the definable well order of the reals it provides are not formalized. | V=L and the definable well order it provides are not formalized. |
modifiedNaturals well ordered by ≤1c497e8df5bd
| Field | From #3198 | To #3709 |
|---|
| note | ℕ under its standard order is a well order (type ω), via `type_nat_lt` and the `WellFoundedLT ℕ` instance. | ℕ with its standard order is a well order (type ω), via `type_nat_lt` and the `WellFoundedLT ℕ` instance. |
modifiedEquivalent formulations of well orderd1b23fe814dd
| Field | From #3198 | To #3709 |
|---|
| note | Individual equivalences exist (`wellFounded_iff_has_min`, `wellFounded_iff_isEmpty_descending_chain`) but not bundled as one TFAE statement. | Individual equivalences exist (`wellFounded_iff_has_min`, `wellFounded_iff_isEmpty_descending_chain`), but not bundled as one TFAE. |
addedDescending chain condition (DCC) characterizationff7c7f3cd8ee
modifiedInitial segment39e8e5f33fe5
| Field | From #3198 | To #3709 |
|---|
| note | `PrincipalSeg.ofElement r a` is the initial segment determined by `a`, with range `Set.Iio a`. | `PrincipalSeg.ofElement r a` gives the initial segment determined by `a`, with range `Set.Iio a`. |
modifiedOrdinal number via initial segmentsc5d5a493ed5a
| Field | From #3198 | To #3709 |
|---|
| note | `ZFSet.IsOrdinal` defines von Neumann ordinals as transitive sets well-ordered by ∈, where each element is its own initial segment. | `ZFSet.IsOrdinal` defines von Neumann ordinals as transitive sets well-ordered by ∈. |
modifiedNot isomorphic to proper initial segmentbb569b2fd7df
| Field | From #3198 | To #3709 |
|---|
| note | `PrincipalSeg.irrefl` shows there is no principal-segment embedding `r ≺i r` of a well order into itself. | `PrincipalSeg.irrefl` rules out any principal-segment embedding `r ≺i r`. |
modifiedComparability of well-ordered sets3e55c7cb8666
| Field | From #3198 | To #3709 |
|---|
| note | `InitialSeg.total` shows of two well orders, one embeds as an initial segment of the other. | `InitialSeg.total` shows for two well orders one embeds as an initial segment of the other. |
modifiedMorphisms preserve initial segments37a1a1c9a2d5
| Field | From #3198 | To #3709 |
|---|
| note | `InitialSeg.image_Iio` shows an initial-segment morphism maps `Set.Iio a` to `Set.Iio (f a)`. | `InitialSeg.image_Iio` shows an initial-segment morphism sends `Set.Iio a` to `Set.Iio (f a)`. |
modifiedOrdering on the class of well-ordered sets2a7d1160d967
| Field | From #3198 | To #3709 |
|---|
| note | `Ordinal` is the class of well orders up to isomorphism carrying a `LinearOrder` defined via initial-segment embeddings. | `Ordinal` is the class of well orders up to isomorphism, carrying a `LinearOrder` defined via initial-segment embeddings. |
modifiedUnion of a chain is well-orderedfe0833a4bcd1
| Field | From #3198 | To #3709 |
|---|
| note | No direct statement that the union of a chain of well-ordered sets (each an initial segment of the next) is well-ordered was found. | No direct statement that the union of a chain of well-ordered sets (with initial-segment inclusions) is itself well-ordered was found. |
modifiedInitial-segment order coincides with inclusion for ordinals88546d0c3b56
| Field | From #3198 | To #3709 |
|---|
| note | The von Neumann ordinal development (∈/⊆ order via `ZFSet.IsOrdinal`) exists, but the exact coincidence statement isn't isolated. | The von Neumann ordinal development via `ZFSet.IsOrdinal` exists, but the exact coincidence statement isn't isolated. |
modifiedOrder topology on a well-ordered setbc2d79a00058
| Field | From #3198 | To #3709 |
|---|
| note | `Preorder.topology` / `OrderTopology` provide the order topology for any (pre)order, hence for well orders. | `Preorder.topology` / `OrderTopology` provide the order topology on any preorder, hence on any well order. |
modifiedIsolated points and limit points48e5dfbb47a9
| Field | From #3198 | To #3709 |
|---|
| note | `Order.IsSuccLimit` captures limit elements (vs successors), but the topological isolated/limit-point dichotomy for well orders isn't separately stated. | `Order.IsSuccLimit` captures limit elements (vs successors), but the topological isolated/limit-point dichotomy isn't isolated. |
modifiedCofinal subset7e07ac34e185
| Field | From #3198 | To #3709 |
|---|
| note | `IsCofinal` (in Mathlib.Order.Bounds.Defs) defines a cofinal set in any ordered type as one with elements ≥ every element (i.e. unbounded). | `IsCofinal` defines a cofinal set in any ordered type as one with elements ≥ every element. |
modifiedOrder type determines cardinalityd93e605f0397
| Field | From #3198 | To #3709 |
|---|
| note | `Ordinal.card` (with `card_type`) is the well-defined map from order type to cardinality; the 'not conversely' direction is not a single theorem. | `Ordinal.card` (with `card_type`) is the well-defined order-type-to-cardinality map; the 'not conversely' direction isn't a single theorem. |
modifiedUncountably many order types for countable sets5f9d09885f8d
| Field | From #3198 | To #3709 |
|---|
| note | The infrastructure of ω₁ and ℵ₁ > ℵ₀ exists, but the specific statement that the countable order types form an uncountable set isn't isolated. | The ω₁ / ℵ₁ > ℵ₀ infrastructure exists but the exact statement that countable order types form an uncountable set is not isolated. |
modifiedTransfinite recursion theorem4c3e616cb278
| Field | From #3198 | To #3709 |
|---|
| note | Transfinite recursion is available via `Ordinal.limitRecOn` (in Mathlib.SetTheory.Ordinal.Arithmetic) and `WellFounded.fix` for defining functions on well-ordered sets by recursion on initial segments. | Transfinite recursion is available via `Ordinal.limitRecOn` and `WellFounded.fix` for defining functions on well-ordered sets by recursion on initial segments. |