OAI/Geometry/TamingCompatibility/Charts/ScalarChartLift.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.ManifoldForms.scalarChartLift line 18
2. def OAI.TamingCompatibility.ManifoldForms.scalarLiftSupport line 22
3. lemma OAI.TamingCompatibility.ManifoldForms.scalarLiftSupport_subset line 26
4. lemma OAI.TamingCompatibility.ManifoldForms.scalarLiftSupport_compact line 33
5. lemma OAI.TamingCompatibility.ManifoldForms.scalarChartLift_zero_off line 39
6. lemma OAI.TamingCompatibility.ManifoldForms.scalarChartLift_apply_inverse line 47
7. lemma OAI.TamingCompatibility.ManifoldForms.scalarChartLift_smooth line 54
8. lemma OAI.TamingCompatibility.ManifoldForms.scalarChartLift_tsupport line 73
9. lemma OAI.TamingCompatibility.ManifoldForms.scalarChartLift_fderiv line 83
10. def OAI.TamingCompatibility.ManifoldForms.vectorChartLift line 104
11. def OAI.TamingCompatibility.ManifoldForms.vectorLiftSupport line 108
12. lemma OAI.TamingCompatibility.ManifoldForms.vectorLiftSupport_subset line 112
13. lemma OAI.TamingCompatibility.ManifoldForms.vectorLiftSupport_compact line 119
14. lemma OAI.TamingCompatibility.ManifoldForms.vectorChartLift_zero_off line 125
15. lemma OAI.TamingCompatibility.ManifoldForms.vectorChartLift_apply_inverse line 133
16. lemma OAI.TamingCompatibility.ManifoldForms.vectorChartLift_smooth line 140