Revision #2855 → #3331 · back to history
modifiedCountable set37821b557cdc
| Field | From #2855 | To #3331 |
|---|
| note | `Set.Countable s` (and the type-level `Countable`) is exactly the notion of a countable set, via an injection into ℕ. | `Set.Countable s` (verified) is exactly the notion of a countable set via an injection into ℕ. |
modifiedCountably infinite set1c8848293d6e
| Field | From #2855 | To #3331 |
|---|
| note | `Denumerable` is a typeclass for types in constructive bijection with ℕ, i.e. countably infinite. | `Denumerable` (verified) is the typeclass for types in constructive bijection with ℕ, i.e. countably infinite. |
modifiedExistence of uncountable sets87248903e05c
| Field | From #2855 | To #3331 |
|---|
| note | `Function.cantor_surjective` proves no surjection α → Set α exists, witnessing uncountable types (and `Uncountable ℝ` is a concrete instance). | `Function.cantor_surjective` (verified) shows no surjection α → Set α exists, witnessing uncountable types. |
modifiedAxiom of countable choice4944cd5e5b8c
| Field | From #2855 | To #3331 |
|---|
| note | Mathlib uses Lean's full classical choice; countable choice is the restriction to countable index families and is a consequence of `Classical.axiomOfChoice`. | Mathlib uses Lean's full classical choice (`Classical.axiomOfChoice`, verified); countable choice is a consequence. |
modifiedCardinality57390b5b22ea
| Field | From #2855 | To #3331 |
|---|
| note | `Cardinal.mk α` (notation `#α`) is the cardinality of a type; countability becomes `#α ≤ ℵ₀`. | `Cardinal.mk α` (verified, notation `#α`) is the cardinality of a type. |
modifiedCountable set (equivalent definitions)ba8a9679aaf0
| Field | From #2855 | To #3331 |
|---|
| note | `countable_iff_exists_injective` characterizes countability by the existence of an injection into ℕ. | `countable_iff_exists_injective` (verified) characterizes countability via an injection into ℕ. |
modifiedAleph-null1a22f8275b27
| Field | From #2855 | To #3331 |
|---|
| note | `Cardinal.aleph0` (notation `ℵ₀`) is the cardinality of ℕ. | `Cardinal.aleph0` (verified, notation `ℵ₀`) is the cardinality of ℕ. |
modifiedDefinitions are equivalent8e0e4792f79e
| Field | From #2855 | To #3331 |
|---|
| note | The injection/surjection characterizations are proved equivalent via `countable_iff_exists_injective` and `countable_iff_exists_surjective`. | `countable_iff_exists_injective` and `countable_iff_exists_surjective` (both verified) give the equivalent characterizations. |
modifiedCountably infinite setdb65e11b3bf4
| Field | From #2855 | To #3331 |
|---|
| note | `Denumerable` captures countably infinite as a constructive bijection with ℕ. | `Denumerable` (verified) captures countably infinite as a constructive bijection with ℕ. |
modifiedUncountable set1ecb4bd6018d
| Field | From #2855 | To #3331 |
|---|
| note | `Uncountable α` is defined as `¬Countable α` (`uncountable_iff_not_countable`). | `Uncountable α` (verified) is defined as `¬Countable α`. |
modifiedIntegers and even integers in correspondence191ec4f88ec3
| Field | From #2855 | To #3331 |
|---|
| note | This specific illustrative bijection between ℤ and the even integers is not stated as a named declaration in Mathlib. | This specific illustrative bijection between ℤ and the even integers is not a named declaration in Mathlib. |
modifiedBijection / one-to-one correspondence3c5aaa9c941a
| Field | From #2855 | To #3331 |
|---|
| note | `Equiv` (with `Function.Bijective` for the predicate form) formalizes a one-to-one correspondence between two types. | `Equiv` (verified) formalizes a one-to-one correspondence between two types. |
modifiedSame cardinality70a0e0d94ea2
| Field | From #2855 | To #3331 |
|---|
| note | `Cardinal.eq` states `#α = #β ↔ Nonempty (α ≃ β)`, i.e. equal cardinality iff a bijection exists. | `Cardinal.eq` (verified) states `#α = #β ↔ Nonempty (α ≃ β)`. |
modifiedCountably infinite (naming)813967ed38e1
| Field | From #2855 | To #3331 |
|---|
| note | `Denumerable` is exactly the typeclass for types in bijection with ℕ. | `Denumerable` (verified) is the typeclass for types in bijection with ℕ. |
modifiedNot all infinite sets are countably infiniteb39f01169b52
| Field | From #2855 | To #3331 |
|---|
| note | ℝ is infinite yet `Cardinal.not_countable_real` (and `Uncountable ℝ`) shows it is not countable, witnessing the claim. | `Cardinal.not_countable_real` (verified) witnesses the claim via ℝ being infinite yet uncountable. |
modifiedReal numbers are uncountabled613900404f9
| Field | From #2855 | To #3331 |
|---|
| note | `Cardinal.mk_real` gives `#ℝ = 𝔠` and `Cardinal.not_countable_real` gives that ℝ exceeds ℵ₀. | `Cardinal.mk_real` (verified) gives `#ℝ = 𝔠`; with `Cardinal.not_countable_real` this shows ℝ exceeds ℵ₀. |
modifiedCantor's diagonal argument1233aacbbdac
| Field | From #2855 | To #3331 |
|---|
| note | Cantor's diagonal argument is captured by `Cardinal.cantor` (`a < 2^a`) and `Function.cantor_surjective`; the specific real-number diagonal yields `Uncountable ℝ`. | `Cardinal.cantor` (`a < 2^a`) and `Function.cantor_surjective` (both verified) capture the diagonal argument. |
modifiedCountable set (formal)a38fa2e72bee
| Field | From #2855 | To #3331 |
|---|
| note | Countability via an injection (bijection onto a subset of ℕ) is `countable_iff_exists_injective`. | `countable_iff_exists_injective` (verified) gives countability as existence of an injection into ℕ. |
modifiedFinite sets are countable19c1c9a700c2
| Field | From #2855 | To #3331 |
|---|
| note | `Set.Finite.countable` (and instance `Finite.to_countable`) shows every finite set/type is countable. | `Set.Finite.countable` (verified) shows every finite set is countable. |
modifiedCountably infinite set (formal)6a1e3309f754
| Field | From #2855 | To #3331 |
|---|
| note | `Denumerable` is the formal bijection-with-ℕ notion of countably infinite. | `Denumerable` (verified) formalizes the bijection-with-ℕ notion. |
modifiedPositive integers and even integers are countably infinite60165a1c8149
| Field | From #2855 | To #3331 |
|---|
| note | `Denumerable.pnat` makes ℕ+ denumerable, but the specific even-integers example is not a separately named declaration. | `Denumerable.pnat` (verified) makes ℕ+ denumerable, but the even-integers example is not a named declaration. |
modifiedCountable iff countably infinite or finitec00beddb62eb
| Field | From #2855 | To #3331 |
|---|
| note | `Set.countable_infinite_iff_nonempty_denumerable` proves that an infinite countable set is denumerable, equating countable-and-infinite with countably-infinite. | `Set.countable_infinite_iff_nonempty_denumerable` (verified) states countable+infinite ↔ denumerable. |
modifiedN×N is countably infinite8b16e3c85d2b
| Field | From #2855 | To #3331 |
|---|
| note | `Denumerable.prod` gives that the product of two denumerable types is denumerable, instantiating to ℕ × ℕ countably infinite. | `Denumerable.prod` (verified) gives products of denumerable types are denumerable, instantiating to ℕ × ℕ. |
modifiedCartesian product49ac85affa0d
| Field | From #2855 | To #3331 |
|---|
| note | `Set.prod` (and the type-level `Prod`) formalizes the Cartesian product of sets/types. | `Set.prod` (verified) formalizes the Cartesian product of sets. |
modifiedAlgebraic numbers are countable4acbac792544
| Field | From #2855 | To #3331 |
|---|
| note | `Algebraic.countable` shows `{x | IsAlgebraic R x}` is countable for countable R, generalizing the algebraic numbers. | `Algebraic.countable` (verified) shows `{x | IsAlgebraic R x}` is countable for countable R. |
modifiedPositive rationals are countableb556b068e807
| Field | From #2855 | To #3331 |
|---|
| note | ℚ is countable (`Rat.instDenumerable`), so by `Subtype.countable` any positive-rationals subtype is countable. | ℚ is denumerable (`Rat.instDenumerable`, verified) and `Subtype.countable` (verified) yields any positive-rationals subtype is countable. |
modifiedPower set3b75b4d68d57
| Field | From #2855 | To #3331 |
|---|
| note | `Set.powerset s = {t | t ⊆ s}` formalizes the power set; the type-level analogue is `Set α` itself. | `Set.powerset` (verified) is `{t | t ⊆ s}`, the power set. |
modifiedCantor's theorem70fdbd1aba83
| Field | From #2855 | To #3331 |
|---|
| note | `Function.cantor_surjective` proves no map α → Set α is surjective; `Cardinal.cantor` states `a < 2^a`. | `Function.cantor_surjective` (verified) proves no map α → Set α is surjective; `Cardinal.cantor` gives `a < 2^a`. |
modifiedReals and infinite sequences of naturals are uncountable4583e65fcb00
| Field | From #2855 | To #3331 |
|---|
| note | `Cardinal.not_countable_real`/`Uncountable ℝ` give the reals uncountable; the ℕ→ℕ sequence case follows from Cantor/cardinality. | `Cardinal.not_countable_real` (verified) gives ℝ uncountable; the ℕ→ℕ case follows via Cantor. |
modifiedSubset of a countable set is countablede90282b44d3
| Field | From #2855 | To #3331 |
|---|
| note | `Set.Countable.mono` shows any subset of a countable set is countable. | `Set.Countable.mono` (verified) shows subsets of countable sets are countable. |
modifiedCartesian product of finitely many countable sets is countable2face1e1b66f
| Field | From #2855 | To #3331 |
|---|
| note | `Set.Countable.prod` covers binary products and `countable_univ_pi` covers finite products of countable sets. | `Set.Countable.prod` (verified) covers binary products; iterating handles finite products. |
modifiedZ and Q are countable49bf9b28496a
| Field | From #2855 | To #3331 |
|---|
| note | `Denumerable.int` and `Rat.instDenumerable` make ℤ and ℚ denumerable, hence countable. | `Denumerable.int` and `Rat.instDenumerable` (both verified) make ℤ and ℚ denumerable, hence countable. |
modifiedFinite union of countable sets is countable76a479ea1237
| Field | From #2855 | To #3331 |
|---|
| note | `Set.Countable.union` handles binary unions; iterating gives any finite union of countable sets. | `Set.Countable.union` (verified) handles binary unions; iteration covers any finite union. |
modifiedUnion of countably many countable sets is countable5448c5729c66
| Field | From #2855 | To #3331 |
|---|
| note | `Set.countable_iUnion` (with `Set.Countable.biUnion`/`Set.Countable.sUnion`) shows a countable union of countable sets is countable. | `Set.countable_iUnion` (verified) shows a countable union of countable sets is countable. |
modifiedSet of finite-length sequences of naturals is countable81b69271ab9f
| Field | From #2855 | To #3331 |
|---|
| note | `Denumerable.denumerableList` makes `List α` denumerable for denumerable α, so `List ℕ` (finite sequences of naturals) is countable. | `Denumerable.denumerableList` (verified) makes `List α` denumerable for denumerable α, so `List ℕ` is countable. |
modifiedSet of finite subsets of naturals is countablec8239f792663
| Field | From #2855 | To #3331 |
|---|
| note | `Set.countable_setOf_finite_subset` shows the finite subsets of a countable set form a countable set. | `Set.countable_setOf_finite_subset` (verified) shows the finite subsets of a countable set form a countable set. |
modifiedInjection/surjection with a countable set4c81ff3f1410
| Field | From #2855 | To #3331 |
|---|
| note | `Function.Injective.countable` (and the surjective counterpart) transfers countability along injections/surjections. | `Function.Injective.countable` (verified) transfers countability along injections; a surjective counterpart exists. |
modifiedThe set is uncountablea878faaf5657
| Field | From #2855 | To #3331 |
|---|
| note | `Cardinal.cantor` (`a < 2^a`) and `Function.cantor_surjective` give that the power set / 2^ℕ is uncountable. | `Cardinal.cantor` (verified, `a < 2^a`) with `Function.cantor_surjective` gives the power set / 2^ℕ uncountable. |
modifiedTotal orders on countable setsef1a79ee7e82
| Field | From #2855 | To #3331 |
|---|
| note | Total orders are formalized as `LinearOrder`, but the informal observation that countable sets admit various total orders is not stated as a theorem. | Total orders are `LinearOrder` (verified), but the informal remark that countable sets admit various total orders is not a named theorem. |
modifiedUsual order of rationals is not a list895f06210609
| Field | From #2855 | To #3331 |
|---|
| note | 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. | Density is `DenselyOrdered` (verified, with ℚ an instance), but the 'not a list / not a well-order' remark is not a named result. |
modifiedWell order (least element)9a312ef210b0
| Field | From #2855 | To #3331 |
|---|
| note | `IsWellOrder` (built on `IsWellFounded`) formalizes a well order, in which every nonempty subset has a least element. | `IsWellOrder` (verified) formalizes a well order. |
modifiedOrdinal number98c2afd2ce87
| Field | From #2855 | To #3331 |
|---|
| note | `Ordinal` in Mathlib formalizes Cantor's ordinal numbers as equivalence classes of well-orders. | `Ordinal` (verified) formalizes Cantor's ordinals as equivalence classes of well-orders. |
modifiedRecursively enumerable set3e0a20273a18
| Field | From #2855 | To #3331 |
|---|
| note | Recursive enumerability (a computability-theoretic notion, weaker than decidability) is not currently formalized as a named notion in Mathlib. | Recursive enumerability is not currently formalized as a named notion in Mathlib. |
modifiedLöwenheim–Skolem theorem575b1071e424
| Field | From #2855 | To #3331 |
|---|
| note | The downward Löwenheim–Skolem theorem is formalized in Mathlib's model-theory library (`FirstOrder.Language.exists_elementarySubstructure_card_eq`). | `FirstOrder.Language.exists_elementarySubstructure_card_eq` (verified) formalizes the downward Löwenheim–Skolem theorem. |
modifiedDedekind-finite setf09eeea1329d
| Field | From #2855 | To #3331 |
|---|
| note | Dedekind-finite (or Dedekind-infinite) sets are not currently formalized as a named notion in Mathlib; the standard `Finite`/`Infinite` classes assume classical choice and coincide with Dedekind-finiteness only under choice. | Dedekind-finite/infinite sets are not currently a named notion in Mathlib; `Finite`/`Infinite` assume classical choice. |
addedInjective functionce0aca8b6f7a
addedNatural numbers2b21fb767cae
addedSurjective function8b8ac01ccc65
addedCantor's first uncountability proof (reals uncountable)2bee7abb01d3