DixmierRegularityFromTopology.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Smooth regularity from the topological Dixmier chart

Given a global exponential homeomorphism, the faithful triangular representation and the injective differential of its exponential prove smoothness of the chart and its inverse, as needed for metric comparison.

theorem OAI.PolycyclicRecognition.dixmier_exponential_smooth_chart line 27
theorem OAI.PolycyclicRecognition.dixmierExponentialDiffeomorphismInput_of_topological line 94
Source documentation
The smooth regularity needed by the metric application is derived; only a global topological exponential chart is a hypothesis.
```
theorem dixmierExponentialDiffeomorphismInput_of_topological
    (dixmier : DixmierExponentialInput (E := E) (G := G)) :
…
```
Mentions: OAI.PolycyclicRecognition.DixmierExponentialInput