OAI/Geometry/TamingCompatibility/DifferentialForms/Wedge.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.ManifoldForms.wedgeOne line 31
2. def OAI.TamingCompatibility.ManifoldForms.wedgeTwo line 33
3. lemma OAI.TamingCompatibility.ManifoldForms.pullback_wedgeOne line 36
4. lemma OAI.TamingCompatibility.ManifoldForms.Smooth.wedgeOne line 45
5. lemma OAI.TamingCompatibility.ManifoldForms.pullback_at_center line 52
6. lemma OAI.TamingCompatibility.ManifoldForms.exteriorDerivative_wedgeOne line 66
7. lemma OAI.TamingCompatibility.ManifoldForms.pullback_wedgeTwo line 79
8. lemma OAI.TamingCompatibility.ManifoldForms.Smooth.wedgeTwo line 85
9. def OAI.TamingCompatibility.GeometricAdjoint.pointMetric line 99
10. def OAI.TamingCompatibility.GeometricAdjoint.pairing line 102
11. lemma OAI.TamingCompatibility.GeometricAdjoint.pairing_neg_right line 106
12. lemma OAI.TamingCompatibility.GeometricAdjoint.coefficient_wedgeTwo_star line 116
13. lemma OAI.TamingCompatibility.GeometricAdjoint.coefficient_wedgeOne_three line 134
14. lemma OAI.TamingCompatibility.GeometricAdjoint.codifferential_smooth line 152
15. theorem OAI.TamingCompatibility.GeometricAdjoint.formal_adjoint line 160