OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialChartBridge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Recovering the topological chart input from the regularity input

Exponential existence is proved by the integral-curve construction. The remaining chart assertion follows from the already required exponential diffeomorphism after changing from finite basis coordinates.

  1. theorem OAI.PolycyclicRecognition.DixmierExponentialDiffeomorphismInput.toTopological line 23