OAI/GroupTheory/PolycyclicRecognition/Geometry/SmoothRotationalTwist.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.rotationalTwistChartedSpace line 22

   Source documentation

   The atlas comes from the original group through the graph projection.

   def rotationalTwistChartedSpace : ChartedSpace E (rotationalTwist α τ hinv) :=
   …

   Mentions: OAI.PolycyclicRecognition.rotationalTwist

2. theorem OAI.PolycyclicRecognition.rotationalTwist_isManifold line 28
3. theorem OAI.PolycyclicRecognition.contMDiff_rotationalTwistProjection line 32
4. theorem OAI.PolycyclicRecognition.contMDiff_rotationalTwistGraph line 37
5. theorem OAI.PolycyclicRecognition.contMDiff_rotationalTwistMul line 45
6. theorem OAI.PolycyclicRecognition.contMDiff_rotationalTwistInv line 64
7. theorem OAI.PolycyclicRecognition.rotationalTwistLieGroup line 83

   Source documentation

   Smoothness of the action along the inverse character is sufficient for both smooth group operations on the graph.

   theorem rotationalTwistLieGroup : LieGroup (𝓘(ℝ,E)) ∞ (rotationalTwist α τ hinv) where
   …

   Mentions: OAI.PolycyclicRecognition.rotationalTwist