Map · 58
global analysis
MSC 58 · Global analysis, analysis on manifolds
4,457 declarations (3,881 theorems, 576 definitions) across 96 files. The 1000+ theorems list has no entries in this area. 2 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.
Subareas2
- 58A General theory of differentiable manifolds 3,150
- 58C Calculus on manifolds; nonlinear operators 1,307
From the 100 theorems list1
Open conjectures stated in Lean2
Statements without proofs, collected by the Formal Conjectures project.
- Hilbert5.hilbert_smith_conjectureHilbert Problems
- Hilbert5.hilbert_smith_padic_formulationHilbert Problems
Structures defined here16
Typeclasses defined in this area's files, most assumed first.
- IsManifold 467
- ContMDiffMul 130
- ContMDiffAdd 68
- ContMDiffRing 50
- HasContDiffBump 50
- DiffeologicalSpace 47
- BoundarylessManifold 32
- ModelWithCorners.Boundaryless 24
- ContMDiffSMul 22
- IsContMDiffRiemannianBundle 22
- ContMDiffVAdd 19
- HasGroupoid 18
- ClosedUnderRestriction 16
- ENat.LEInfty 11
- Diffeology.IsContDiffCompatible 10
- Diffeology.IsDTopologyCompatible 3
Files96
Largest first. The code after each file is its assigned subarea.
- Mathlib.Analysis.Calculus.FDeriv.Add
Additive operations on derivatives
58C · 224
- Mathlib.Geometry.Manifold.MFDeriv.Basic
Basic properties of the manifold Fréchet derivative
58A · 192
- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Differentiability of specific functions
58A · 185
- Mathlib.Geometry.Manifold.Algebra.Monoid
`C^n` monoid
58A · 160
- Mathlib.Analysis.Calculus.FDeriv.Basic
The Fréchet derivative: basic properties
58C · 155
- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Extended charts in smooth manifolds
58A · 153
- Mathlib.Geometry.Manifold.IsManifold.Basic
`C^n` manifolds (possibly with boundary or corners)
58A · 150
- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorphisms
58A · 118
- Mathlib.Geometry.Diffeology.Basic
Diffeological spaces
58A · 109
- Mathlib.Geometry.Manifold.ContMDiff.Defs
`C^n` functions between manifolds
58A · 106
- Mathlib.Geometry.Manifold.Immersion
Smooth immersions
58A · 97
- Mathlib.Geometry.Manifold.LocalInvariantProperties
Local properties invariant under a groupoid
58A · 88