OAI/Geometry/WeakMTW/Potentials/PotentialGraphGlobal.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.WeakMTWGlobalSupport.WeakMTW.potentialGraph_compactline 21 - theorem
OAI.WeakMTWGlobalSupport.WeakMTW.minimizing_pole_ordinaryline 41 - theorem
OAI.WeakMTWGlobalSupport.WeakMTW.potentialProjection_surjectiveline 57 - theorem
OAI.WeakMTWGlobalSupport.WeakMTW.potentialProjection_injectiveline 75 - theorem
OAI.WeakMTWGlobalSupport.WeakMTW.potentialProjection_homeomorphline 100 - theorem
OAI.WeakMTWGlobalSupport.WeakMTW.globalSupportingPropertyline 110