Manifolds and cell complexes
The Lean Pool projects whose card's first MSC2020 code is in class 57, Manifolds and cell complexes: 3 articles, one per card.
TheoremThe classification of compact 1-manifolds#
A Lean 4 (mathlib) proof of the classification of 1-manifolds, specifically that every compact, connected, Hausdorff topological space charted on the half-line [0,∞) is homeomorphic to the circle S¹ or to the closed unit interval [0,1]. The proof follows David Gale's outline: shrink to a finite atlas of interval charts, then induct on the atlas size, merging two overlapping charts at each step; a connected overlap glues two charts into one (two boundary charts glue onto [0, 1]), while a disconnected overlap has exactly two components and yields the circle.
Quoted from the card LeanPool/projects/1mfld.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
OneMfld.homeomorph_circle_or_unitInterval(theorem; a main declaration), declared in LeanPool/OneManifold/Solution.lean, line 26: “Every compact connected Hausdorff space charted on the nonnegative real half-line is homeomorphic to the circle or the closed unit interval.”
Project
- Authors: Jim Fowler, Dennis Sweeney.
- Project repository: sweeneyde/1mfld, at commit 83e961ba.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 57N99, 54F65, 68V20.
- In Lean Pool: LeanPool/OneManifold, from the card LeanPool/projects/1mfld.yaml.
Sources
TheoremClassification of Compact Surfaces#
Formalizes the classification of compact connected Hausdorff topological 2-manifolds with boundary as the sphere, an orientable normal-form quotient, or a non-orientable normal-form quotient, using triangulation and finite cyclic polygonal presentations.
Quoted from the card LeanPool/projects/classification-of-surfaces.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
LeanEval.Topology.ClassificationOfSurfaces.classification_of_surfaces(theorem; a main declaration), declared in LeanPool/ClassificationOfSurfaces/EvalStatement.lean, line 30: “Every compact connected Hausdorff topological 2-manifold with boundary is homeomorphic to the sphere, an orientable normal-form quotient, or a non-orientable normal-form quotient.”
Project
- Authors: Ryan McCorvie, Jack McCarthy, SF Lean Meetup contributors.
- Source: Classification of Compact Surfaces, https://github.com/mccorvie/classification-of-surfaces/tree/master/ClassificationOfSurfaces.
- Project repository: mccorvie/classification-of-surfaces.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 57K20, 57N05.
- In Lean Pool: LeanPool/ClassificationOfSurfaces, from the card LeanPool/projects/classification-of-surfaces.yaml.
Sources
TheoremJordan–Schönflies theorem#
Formalizes the Jordan curve theorem and the extension of every homeomorphism between Jordan curves to a plane homeomorphism.
Quoted from the card LeanPool/projects/schoenflies.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
Schoenflies.jordan_schoenflies_of_homeomorph(theorem; a main declaration), declared in LeanPool/Schoenflies/JordanSchoenflies.lean, line 64: “Every homeomorphism between two Jordan curves in the plane extends to a self-homeomorphism of the plane.”Schoenflies.jordan_schoenflies(theorem), declared in LeanPool/Schoenflies/JordanSchoenflies.lean, line 50: “A homeomorphism between Jordan curves extends to a global homeomorphism agreeing with it on the source curve.”Schoenflies.forall_isSeparating_of_isJordanCurve(theorem), declared in LeanPool/Schoenflies/InitialPairFixed.lean, line 94: “Every Jordan curve separates the plane into an inside and an outside region.”
Project
- Authors: Álvaro Begué.
- Source: The Jordan–Schönflies theorem in Lean.
- Project repository: alonamaloh/schoenflies-lean, at commit 05a43d29.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 57K10, 54C25.
- In Lean Pool: LeanPool/Schoenflies, from the card LeanPool/projects/schoenflies.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.