Revision #1025 → #1724 · back to history
modifiedAxiom of choice (informal)5602deb11b35
| Field | From #1025 | To #1724 |
|---|
| mathlib.module | Mathlib.Logic.Basic | Init.Classical |
| note | Mathlib's Classical.axiomOfChoice yields a choice function from a family of nonempty types. | Classical.axiomOfChoice yields a choice function from a family of nonempty types. |
modifiedSmallest element of finite subsets of naturals78b1fae2c086
| Field | From #1025 | To #1724 |
|---|
| note | This is a numeric illustrative example, not a formalizable mathematical statement. | Illustrative numeric example, not a formalizable mathematical statement. |
modifiedRussell's shoes and socks analogydc329736cd0d
| Field | From #1025 | To #1724 |
|---|
| note | An informal pedagogical analogy with no formal counterpart. | Informal pedagogical analogy with no formal counterpart. |
modifiedChoice function0b6aedf4688e
| Field | From #1025 | To #1724 |
|---|
| mathlib.module | Mathlib.Logic.Basic | Init.Classical |
modifiedAxiom of choice (formal axiom box)f273aebc3ddd
| Field | From #1025 | To #1724 |
|---|
| mathlib.module | Mathlib.Logic.Basic | Init.Classical |
| note | The existence of a choice function for nonempty sets is Classical.axiomOfChoice (built on Lean's Classical.choice). | Existence of a choice function for nonempty sets is Classical.axiomOfChoice. |
modifiedEquivalent form via Cartesian productd1c206ed2fd9
| Field | From #1025 | To #1724 |
|---|
| note | Classical.nonempty_pi states Nonempty (∀ i, π i) ↔ ∀ i, Nonempty (π i), i.e. the product of nonempty sets is nonempty. | Classical.nonempty_pi: Nonempty (∀ i, π i) ↔ ∀ i, Nonempty (π i), i.e. the product of nonempty sets is nonempty. |
modifiedPartition/transversal variant7049a0bfdff7
| Field | From #1025 | To #1724 |
|---|
| mathlib.module | Mathlib.Logic.Basic | Init.Classical |
| note | The choice axiom is present, but there is no dedicated lemma producing a transversal of a partition. | Choice is present, but no dedicated lemma produces a transversal of a partition. |
modifiedPowerset choice-function varianta7e709bc57ae
| Field | From #1025 | To #1724 |
|---|
| mathlib.module | Mathlib.Logic.Basic | Init.Classical |
| note | Per-nonempty-subset choice is available via choice, but no packaged powerset choice-function object exists. | Per-nonempty-subset choice is available via Classical.axiomOfChoice, but no packaged powerset choice-function object exists. |
modifiedFinite collections need no choice (induction)6206ab5a045e
| Field | From #1025 | To #1724 |
|---|
| note | The nonempty-product lemma covers the finite case, but Mathlib does not isolate a choice-free finite-induction version. | Nonempty-product covers the finite case, but Mathlib does not isolate a choice-free finite-induction version. |
modifiedCanonical choice via explicit rulee35685ff3016
| Field | From #1025 | To #1724 |
|---|
| note | An illustrative discussion rather than a formal statement. | Illustrative discussion rather than a formal statement. |
modifiedSubsets of reals require choice9b02ecb1bed1
| Field | From #1025 | To #1724 |
|---|
| note | An illustrative remark about when choice is needed, not a formal statement. | Illustrative remark, not a formal statement. |
modifiedOpen interval has no least elementedf1a31906f7
| Field | From #1025 | To #1724 |
|---|
| note | No dedicated lemma stating that an open real interval has no least element was found. | No dedicated lemma stating an open real interval has no least element was found. |
modifiedWell-ordering of reals equivalent to choice function69efad273aea
| Field | From #1025 | To #1724 |
|---|
| mathlib.decl | Cardinal.exists_wellFoundedLT | exists_wellOrder |
| note | The general well-ordering theorem applies to ℝ, but the stated equivalence with a choice function for sets of reals is not a separate decl. | The general well-ordering theorem applies to ℝ via exists_wellOrder, but the stated equivalence with a choice function for sets of reals is not a separate decl. |
modifiedConstruction of a non-measurable setb2c69fb40b64
| Field | From #1025 | To #1724 |
|---|
| note | The Vitali non-measurable set construction is not in Mathlib (docs/1000.yaml points to an external repository). | The Vitali non-measurable set construction is not in Mathlib. |
modifiedDiaconescu's theorem9f9dd2eec892
| Field | From #1025 | To #1724 |
|---|
| mathlib.module | Mathlib.Logic.Basic | Init.Classical |
| note | Lean derives Classical.em from Classical.choice via Diaconescu's argument; Mathlib re-exports it as the alias em. | Lean derives Classical.em from Classical.choice via Diaconescu's argument. |
modifiedGlobal choice from limitation of size855b142f8d3a
| Field | From #1025 | To #1724 |
|---|
| note | The axiom of limitation of size and its implications are not formalized in Mathlib. | Limitation of size and its implications are not formalized in Mathlib. |
modifiedTarski's axiom stronger than AC3f33098b649c
| Field | From #1025 | To #1724 |
|---|
| note | Tarski's axiom (existence of inaccessibles/universes) as a set-theoretic statement is not formalized in Mathlib. | Tarski's axiom as a set-theoretic statement is not formalized in Mathlib. |
modifiedTrichotomy of cardinalitiese86aabd8f71d
| Field | From #1025 | To #1724 |
|---|
| note | Cardinal forms a LinearOrder (its le_total field), so any two cardinalities are comparable. | Cardinal forms a LinearOrder, so any two cardinalities are comparable. |
modifiedEvery surjection has a right inverse040142117195
| Field | From #1025 | To #1724 |
|---|
| note | A surjection has a right inverse via Function.surjInv / Function.Surjective.hasRightInverse. | A surjection has a right inverse via Function.Surjective.hasRightInverse. |
modifiedDisjoint collection has transversalfdfe1eb2dfd6
| Field | From #1025 | To #1724 |
|---|
| mathlib.module | Mathlib.Logic.Basic | Init.Classical |
modifiedRelation contains a functiona57e77e7822f
| Field | From #1025 | To #1724 |
|---|
| mathlib.module | Mathlib.Logic.Basic | Init.Classical |
modifiedMaximal collection with finite intersection property26a865cc8a7c
| Field | From #1025 | To #1724 |
|---|
| note | Tukey's lemma gives maximal finite-character families, but the finite-intersection-property phrasing is not a separate decl. | Tukey's lemma gives maximal finite-character families, but the FIP phrasing is not a separate decl. |
modifiedWell-ordering theorem6a45bf369f37
| Field | From #1025 | To #1724 |
|---|
| mathlib.decl | Cardinal.exists_wellFoundedLT | exists_wellOrder |
| note | Zermelo's well-ordering theorem; any type also gets the concrete well-order WellOrderingRel. | exists_wellOrder (and the concrete WellOrderingRel) is Zermelo's well-ordering theorem. |
modifiedPowerset of an ordinal is well-orderablec51d2e5959f0
| Field | From #1025 | To #1724 |
|---|
| mathlib.decl | Cardinal.exists_wellFoundedLT | exists_wellOrder |
modifiedEvery vector space has a basisc85afe705eba
| Field | From #1025 | To #1724 |
|---|
| mathlib.decl | Basis.ofVectorSpace | Module.Basis.ofVectorSpace |
| note | Basis.ofVectorSpace builds a basis for any vector space over a division ring. | Module.Basis.ofVectorSpace builds a basis for any vector space over a division ring. |
modifiedBaer's criterion (divisible implies injective)bfa5f89f5b11
| Field | From #1025 | To #1724 |
|---|
| note | Module.Baer.injective is the general Baer criterion; combined with Module.Baer.of_divisible it gives divisible → injective. | Module.Baer.injective is the general Baer criterion, giving divisible → injective for ℤ-modules. |
modifiedEvery set is a projective object in Set1b640343c32b
| Field | From #1025 | To #1724 |
|---|
| mathlib.decl | CategoryTheory.Type.enoughProjectives | CategoryTheory.Projective.Type.enoughProjectives |
| note | An instance makes every type a projective object (docstring: 'the axiom of choice says every type is a projective object in Type'). | An instance makes the category Type have enough projectives — every type is projective in Type. |
modifiedMaximal consistent superset of first-order sentencesc2cef7b69463
| Field | From #1025 | To #1724 |
|---|
| note | Maximal theories are defined and obtained from models (completeTheory), but a general Lindenbaum extension lemma is not present. | Maximal theories are defined and obtainable from models, but a general Lindenbaum extension lemma is not present. |
modifiedLöwenheim–Skolem theoremfa3ef0f1a9e6
| Field | From #1025 | To #1724 |
|---|
| note | The downward Löwenheim–Skolem theorem is formalized (with an upward companion in Satisfiability). | Downward Löwenheim–Skolem theorem is formalized. |
modifiedEvery connected graph has a spanning tree147ece39d68f
| Field | From #1025 | To #1724 |
|---|
| note | SimpleGraph.IsTree is defined, but there is no theorem producing a spanning tree of an arbitrary connected graph. | SimpleGraph.IsTree is defined, but no theorem produces a spanning tree of an arbitrary connected graph. |
modifiedInfinite set has countable-infinite subset70449e8fbb54
| Field | From #1025 | To #1724 |
|---|
| note | Built on Infinite.natEmbedding, this gives a countably infinite subset of any infinite set. | Gives a countably infinite subset of any infinite set. |
modifiedVitali theorem (non-measurable sets)62eb73f46dbf
| Field | From #1025 | To #1724 |
|---|
| note | The Vitali set / existence of a non-measurable set is not in Mathlib (only Vitali covering theory). | The Vitali set / existence of a non-measurable set is not in Mathlib. |
modifiedInfinite-dimensional spaces have infinite independent subsetdf6d3e93a80f
| Field | From #1025 | To #1724 |
|---|
| mathlib.decl | Basis.ofVectorSpace | Module.Basis.ofVectorSpace |
modifiedCompactness: topological = sequential4ca875ec55e4
| Field | From #1025 | To #1724 |
|---|
| note | isCompact_iff_isSeqCompact equates compactness with sequential compactness (e.g. for metric spaces). | isCompact_iff_isSeqCompact equates compactness with sequential compactness on sequential spaces. |
modifiedBaire category theorem3a9d0fdd46ab
| Field | From #1025 | To #1724 |
|---|
| note | Complete (pseudo)metrizable spaces are Baire spaces; conclusion lemmas are in Topology.Baire.Lemmas. | Complete (pseudo)metrizable spaces are Baire spaces. |
modifiedUrysohn's lemma127fc595ef84
| Field | From #1025 | To #1724 |
|---|
| note | Urysohn's lemma is exists_continuous_zero_one_of_isClosed for disjoint closed sets in a normal space. | Urysohn's lemma for disjoint closed sets in a normal space. |
modifiedGödel's completeness theoremb3662b0f86f1
| Field | From #1025 | To #1724 |
|---|
| note | Mathlib's ModelTheory has no syntactic proof system, so the soundness/completeness theorem is not formalized. | Mathlib's ModelTheory has no syntactic proof system, so soundness/completeness is not formalized. |
modifiedCompactness theorembe382a369623
| Field | From #1025 | To #1724 |
|---|
| note | The first-order compactness theorem is isSatisfiable_iff_isFinitelySatisfiable. | The first-order compactness theorem. |
modifiedInjection or surjection between two setsbdec41b9aa02
| Field | From #1025 | To #1724 |
|---|
| note | Cardinal comparability (le_total) gives an injection one way; the injection-or-surjection phrasing is not a dedicated decl. | Cardinal comparability gives an injection one way; the injection-or-surjection phrasing is not a dedicated decl. |
modifiedNo infinite decreasing sequence of cardinalsa1fe9a2dcc5b
| Field | From #1025 | To #1724 |
|---|
| note | Cardinal.lt_wf (and WellFoundedLT Cardinal) shows < on cardinals is well-founded, ruling out infinite descent. | Cardinal.lt_wf shows < on cardinals is well-founded, ruling out infinite descent. |
modifiedBaire property of all reals stronger than ¬AC587b2c8276d4
| Field | From #1025 | To #1724 |
|---|
| note | The statement that every set of reals has the Baire property is not formalized in Mathlib. | Not formalized in Mathlib. |
modifiedAxiom of choice in type theory0ea9cebe7b69
| Field | From #1025 | To #1724 |
|---|
| mathlib.module | Mathlib.Logic.Basic | Init.Classical |
| note | The type-theoretic choice (∀x ∃y R x y → ∃f ∀x R x (f x)) is exactly Classical.axiomOfChoice / Classical.skolem. | Type-theoretic choice (∀x ∃y R x y → ∃f ∀x R x (f x)) is exactly Classical.axiomOfChoice. |
addedAxiom of choice formulated by Zermelo (1904)3957017ec137
addedZermelo–Fraenkel set theory with choice (ZFC)0811e3e37ed8
addedAxiom of determinacy7add12ce52ff