Revision #1707 → #2192 · back to history
modifiedCountably infinite set1c8848293d6e
| Field | From #1707 | To #2192 |
|---|
| mathlib.match_kind | generalization | exact |
| note | `Denumerable` is a type constructively in bijection with ℕ, i.e. countably infinite (and `nonempty_denumerable_iff` shows this equals Countable ∧ Infinite). | `Denumerable` is a typeclass for types in constructive bijection with ℕ, i.e. countably infinite. |
modifiedExistence of uncountable sets87248903e05c
| Field | From #1707 | To #2192 |
|---|
| note | Cantor's diagonal `Function.cantor_surjective` proves no surjection α → Set α exists, witnessing uncountable types (also `Uncountable ℝ`). | `Function.cantor_surjective` proves no surjection α → Set α exists, witnessing uncountable types (and `Uncountable ℝ` is a concrete instance). |
addedAxiom of countable choice4944cd5e5b8c
addedCardinality57390b5b22ea
modifiedCountable set (equivalent definitions)ba8a9679aaf0
| Field | From #1707 | To #2192 |
|---|
| note | `countable_iff_exists_injective` characterizes countability by an injection into ℕ. | `countable_iff_exists_injective` characterizes countability by the existence of an injection into ℕ. |
addedAleph-null1a22f8275b27
modifiedCountably infinite setdb65e11b3bf4
| Field | From #1707 | To #2192 |
|---|
| mathlib.match_kind | generalization | exact |
modifiedUncountable set1ecb4bd6018d
| Field | From #1707 | To #2192 |
|---|
| note | `Uncountable` is defined as `¬Countable α` (`uncountable_iff_not_countable`). | `Uncountable α` is defined as `¬Countable α` (`uncountable_iff_not_countable`). |
modifiedBijection / one-to-one correspondence3c5aaa9c941a
| Field | From #1707 | To #2192 |
|---|
| note | `Equiv` (and `Function.Bijective`) formalizes a one-to-one correspondence between two types. | `Equiv` (with `Function.Bijective` for the predicate form) formalizes a one-to-one correspondence between two types. |
modifiedCountably infinite (naming)813967ed38e1
| Field | From #1707 | To #2192 |
|---|
| mathlib.match_kind | generalization | exact |
modifiedNot all infinite sets are countably infiniteb39f01169b52
| Field | From #1707 | To #2192 |
|---|
| note | ℝ is infinite yet `Cardinal.not_countable_real`/`Uncountable ℝ` shows it is not countable, witnessing the claim. | ℝ is infinite yet `Cardinal.not_countable_real` (and `Uncountable ℝ`) shows it is not countable, witnessing the claim. |
modifiedReal numbers are uncountabled613900404f9
| Field | From #1707 | To #2192 |
|---|
| note | `Cardinal.mk_real` gives `#ℝ = 𝔠` and `Cardinal.not_countable_real` that ℝ exceeds ℵ₀. | `Cardinal.mk_real` gives `#ℝ = 𝔠` and `Cardinal.not_countable_real` gives that ℝ exceeds ℵ₀. |
addedCantor's diagonal argument1233aacbbdac
modifiedCountably infinite set (formal)6a1e3309f754
| Field | From #1707 | To #2192 |
|---|
| mathlib.match_kind | generalization | exact |
modifiedPositive integers and even integers are countably infinite60165a1c8149
| Field | From #1707 | To #2192 |
|---|
| note | `Denumerable ℕ+` gives positive integers countably infinite, but the even-integers example set is not a separately named declaration. | `Denumerable.pnat` makes ℕ+ denumerable, but the specific even-integers example is not a separately named declaration. |
modifiedCountable iff countably infinite or finitec00beddb62eb
| Field | From #1707 | To #2192 |
|---|
| note | `Set.countable_infinite_iff_nonempty_denumerable` proves an infinite countable set is denumerable (countably infinite). | `Set.countable_infinite_iff_nonempty_denumerable` proves that an infinite countable set is denumerable, equating countable-and-infinite with countably-infinite. |
modifiedN×N is countably infinite8b16e3c85d2b
| Field | From #1707 | To #2192 |
|---|
| note | `Denumerable.prod` (and `Nat.pairEquiv : ℕ × ℕ ≃ ℕ`) gives that ℕ × ℕ is countably infinite. | `Denumerable.prod` gives that the product of two denumerable types is denumerable, instantiating to ℕ × ℕ countably infinite. |
addedCartesian product49ac85affa0d
modifiedPositive rationals are countableb556b068e807
| Field | From #1707 | To #2192 |
|---|
| note | ℚ is countable (`Rat.instDenumerable`), so the positive-rationals subtype is countable by `Subtype.countable`. | ℚ is countable (`Rat.instDenumerable`), so by `Subtype.countable` any positive-rationals subtype is countable. |
addedPower set3b75b4d68d57
modifiedFinite union of countable sets is countable76a479ea1237
| Field | From #1707 | To #2192 |
|---|
| note | `Set.Countable.union` handles binary unions; `countable_iUnion` over a `Countable` (hence finite) index covers finite unions. | `Set.Countable.union` handles binary unions; iterating gives any finite union of countable sets. |
modifiedUnion of countably many countable sets is countable5448c5729c66
| Field | From #1707 | To #2192 |
|---|
| note | `Set.countable_iUnion` (with `Countable.biUnion`/`sUnion`) shows a countable union of countable sets is countable. | `Set.countable_iUnion` (with `Set.Countable.biUnion`/`Set.Countable.sUnion`) shows a countable union of countable sets is countable. |
modifiedSet of finite-length sequences of naturals is countable81b69271ab9f
| Field | From #1707 | To #2192 |
|---|
| mathlib.decl | denumerableList | Denumerable.denumerableList |
| note | `denumerableList` makes `List α` denumerable for denumerable α, so `List ℕ` (finite sequences of naturals) is countable. | `Denumerable.denumerableList` makes `List α` denumerable for denumerable α, so `List ℕ` (finite sequences of naturals) is countable. |
modifiedSet of finite subsets of naturals is countablec8239f792663
| Field | From #1707 | To #2192 |
|---|
| note | `Set.countable_setOf_finite_subset` shows the finite subsets of a countable set form a countable set (also `Denumerable (Finset ℕ)`). | `Set.countable_setOf_finite_subset` shows the finite subsets of a countable set form a countable set. |
modifiedInjection/surjection with a countable set4c81ff3f1410
| Field | From #1707 | To #2192 |
|---|
| note | `Function.Injective.countable` and `Function.Surjective.countable` transfer countability along injections/surjections. | `Function.Injective.countable` (and the surjective counterpart) transfers countability along injections/surjections. |
modifiedContents of the minimal standard model735f94524539
| Field | From #1707 | To #2192 |
|---|
| note | The structure/contents of the minimal standard model of set theory is not formalized in Mathlib. | The contents of the minimal standard model of set theory are not formalized in Mathlib. |
modifiedTotal orders on countable setsef1a79ee7e82
| Field | From #1707 | To #2192 |
|---|
| mathlib.module | Mathlib.Order.Defs | Mathlib.Order.Defs.LinearOrder |
| note | Total orders are formalized as `LinearOrder`, but the informal observation that countable sets admit various total orders is not a stated theorem. | Total orders are formalized as `LinearOrder`, but the informal observation that countable sets admit various total orders is not stated as a theorem. |
modifiedUsual order of rationals is not a list895f06210609
| Field | From #1707 | To #2192 |
|---|
| mathlib.module | Mathlib.Order.Defs | Mathlib.Order.Basic |
| note | Density of an order is formalized as `DenselyOrdered` (ℚ is an instance), but the informal 'not a list / not a well-order' remark is not a named result. | Density of an order is formalized as `DenselyOrdered` (with ℚ an instance), but the informal 'not a list / not a well-order' remark is not a named result. |
modifiedWell order (least element)9a312ef210b0
| Field | From #1707 | To #2192 |
|---|
| mathlib.match_kind | generalization | exact |