OAI/GroupTheory/PolycyclicRecognition/Geometry/LocalParameterSmoothness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Testing smoothness in local parameters

A smooth parametrization with invertible derivative supplies local smooth coordinates, by the ordinary inverse function theorem.

  1. theorem OAI.PolycyclicRecognition.contMDiffAt_of_local_parameterization line 26