OAI/Geometry/TamingCompatibility/DifferentialForms/Dpos2.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.UniformJets.dpos_eq_at line 18
2. lemma OAI.TamingCompatibility.GeometricHilbert.UniformJets.dpos_contDiffAt line 24
3. lemma OAI.TamingCompatibility.GeometricHilbert.UniformJets.compact_tube line 29
4. lemma OAI.TamingCompatibility.GeometricHilbert.UniformJets.local_linear_bound line 39
5. lemma OAI.TamingCompatibility.GeometricHilbert.UniformJets.local_quadratic_bound line 60
6. lemma OAI.TamingCompatibility.GeometricHilbert.UniformJets.slice_fderiv_contDiffAt line 93
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalMap_joint line 113
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalDifferential_joint line 119
9. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.regularSet line 129
10. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.regularSet_open line 134
11. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.regularSet_center line 142
12. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pulledA_joint line 148
13. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pulledB_joint line 165