OAI/Geometry/TamingCompatibility/DifferentialForms/ChristoffelCLM.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.NormalJets.christoffelCLM line 36
2. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.christoffelCLM_apply line 56
3. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.christoffel_contDiff line 59
4. def OAI.TamingCompatibility.GeometricHilbert.NormalJets.jointJet line 63
5. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.jointJet_contDiff line 66
6. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.jointJet_hasFDerivAt line 71
7. def OAI.TamingCompatibility.GeometricHilbert.NormalJets.centeredMap line 83
8. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.centeredMap_contDiff line 87
9. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.centeredMap_hasFDerivAt line 93
10. def OAI.TamingCompatibility.GeometricHilbert.NormalJets.centeredDerivative line 105
11. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.centeredMap_hasStrictFDerivAt line 108
12. def OAI.TamingCompatibility.GeometricHilbert.NormalJets.centeredChart line 117
13. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.centeredChart_mem_source line 124
14. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.centeredChart_mem_target line 131
15. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.centeredChart_symm_center line 140
16. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.centeredChart_symm_contDiffAt line 149