OAI/Geometry/TamingCompatibility/Hodge/HodgeCoordinateRetraction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.coordinateEncode line 20
2. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.coordinateDecode line 24
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.coordinateEncode_smooth line 30
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.coordinateDecode_smooth line 40
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.coordinateEncode_rawVector line 55
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.coordinateDecode_apply line 70
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.coordinateDecode_rawVector line 80
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.coordinateDecode_encode_raw line 101
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.coordinateDecode_encode line 114