OAI/Geometry/TamingCompatibility/Charts/EuclideanCoordinateLine.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.unitChart_eval_raw line 16
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitCoordinate_rawVector line 50
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitCoordinate_directionCoordinates line 59
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitCoordinate_wedgeTransform line 84
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitCoordinate_normalized_wedgeTransform line 100
6. def OAI.TamingCompatibility.UnitaryFrame.exteriorTransform line 129
7. lemma OAI.TamingCompatibility.UnitaryFrame.exteriorTransform_smooth line 132
8. lemma OAI.TamingCompatibility.UnitaryFrame.exteriorTransform_frame line 137
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.euclidean_transport_linear line 157
10. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.euclidean_transport_difference line 178