OAI/Geometry/WeakMTW/Main.lean
0 declarations, 0 contain sorry, 0 declared as axioms
This file declares nothing itself. It gathers the 8 imports below, so a file that imports it gets all of them.
Imports
- Mathlib
- OAI.Geometry.WeakMTW.Coordinates.CoordinateIdentification
- OAI.Geometry.WeakMTW.Coordinates.NormalAction
- OAI.Geometry.WeakMTW.Potentials.GlobalSupportTheorem
- OAI.Geometry.WeakMTW.Potentials.LiftedSectionsTheorem
- OAI.Geometry.WeakMTW.Potentials.IntermediateDefinitions
- OAI.Geometry.WeakMTW.Potentials.ParametricEnvelopeBounds
- OAI.Geometry.WeakMTW.Endpoints