Map · 57
manifolds
MSC 57 · Manifolds and cell complexes
291 declarations (196 theorems, 95 definitions) across 7 files. 1 of the 20 famous theorems listed for this area are in Mathlib (5%). 5 open conjectures here are stated in Lean.
Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.
Subareas3
- 57R Differential topology 149
- 57N Topological manifolds 95
- 57S Topological transformation groups 47
Famous theorems1 of 20
From the 1000+ theorems project, which classifies each theorem by MSC area.
Open conjectures stated in Lean5
Statements without proofs, collected by the Formal Conjectures project.
- BingBorsuk.bing_borsuk_conjectureWikipedia
- Hilbert5.hilbert_smith_conjectureHilbert Problems
- Hilbert5.hilbert_smith_padic_formulationHilbert Problems
- PoincareConjecture.poincare_conjecture.variants.smooth_dimension_fourMillennium Prize Problems
- PoincareConjecture.poincare_conjecture.variants.smooth_other_casesMillennium Prize Problems
Structures defined here3
Typeclasses defined in this area's files, most assumed first.
Files7
Largest first. The code after each file is its assigned subarea.
- Mathlib.Geometry.Manifold.PartitionOfUnity
Smooth partition of unity
57R · 111
- Mathlib.Geometry.Manifold.ChartedSpace
Charted spaces
57N · 94
- Mathlib.Topology.Algebra.ProperAction.Basic
Proper group action
57S · 39
- Mathlib.Geometry.Manifold.Bordism
(Unoriented) bordism theory
57R · 38
- Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
When a proper action is properly discontinuous
57S · 6
- Mathlib.Topology.Algebra.ProperAction.Torsor
The action underlying a topological torsor is proper.
57S · 2
- Mathlib.Geometry.Manifold.PoincareConjecture
Statement of the generalized Poincaré conjecture
57N · 1