OAI/Geometry/TamingCompatibility/DifferentialForms/GeometricFrameTest.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricChart.coordinateTest line 21
2. lemma OAI.TamingCompatibility.GeometricChart.coordinateTest_support line 26
3. lemma OAI.TamingCompatibility.GeometricChart.coordinateTest_smooth line 31
4. lemma OAI.TamingCompatibility.GeometricChart.coordinateTest_anti line 38
5. def OAI.TamingCompatibility.GeometricChart.manifoldTest line 62
6. lemma OAI.TamingCompatibility.GeometricChart.manifoldTest_smooth line 66
7. lemma OAI.TamingCompatibility.GeometricChart.manifoldTest_anti line 74
8. lemma OAI.TamingCompatibility.GeometricChart.pullback_manifoldTest line 79
9. abbrev OAI.TamingCompatibility.ScalarPair.F line 94
10. def OAI.TamingCompatibility.ScalarPair.inject line 96
11. lemma OAI.TamingCompatibility.ScalarPair.inject_apply line 100
12. def OAI.TamingCompatibility.ScalarPair.make line 103
13. lemma OAI.TamingCompatibility.ScalarPair.make_apply line 106
14. lemma OAI.TamingCompatibility.ScalarPair.make_norm_sq line 110
15. lemma OAI.TamingCompatibility.ScalarPair.postcomp_derivative line 115
16. lemma OAI.TamingCompatibility.ScalarPair.make_derivative line 125
17. lemma OAI.TamingCompatibility.GeometricChart.scalar_add line 140
18. lemma OAI.TamingCompatibility.GeometricChart.scalar_smul line 149
19. def OAI.TamingCompatibility.GeometricChart.scalarLinear line 157
20. def OAI.TamingCompatibility.GeometricChart.pairLinear line 166
21. lemma OAI.TamingCompatibility.GeometricChart.pairLinear_eq_make line 170