OAI/Geometry/TamingCompatibility/DifferentialForms/SingleFamily.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.FormMetric.singleFamily line 29
2. lemma OAI.TamingCompatibility.FormMetric.singleFamily_orthonormal line 32
3. def OAI.TamingCompatibility.FormMetric.singleBasis line 38
4. lemma OAI.TamingCompatibility.FormMetric.singleBasis_repr line 44
5. lemma OAI.TamingCompatibility.FormMetric.pairing_one line 50
6. lemma OAI.TamingCompatibility.WedgePairing.top_ext line 65
7. lemma OAI.TamingCompatibility.WedgePairing.wedgeTwo_on_frame line 70
8. lemma OAI.TamingCompatibility.WedgePairing.volume_on_frame line 85
9. lemma OAI.TamingCompatibility.WedgePairing.wedgeTwo_star line 93
10. lemma OAI.TamingCompatibility.WedgePairing.wedgeOne_three line 102
11. lemma OAI.TamingCompatibility.WedgePairing.wedgeTwo_star_intrinsic line 120
12. lemma OAI.TamingCompatibility.WedgePairing.wedgeOne_three_intrinsic line 127
13. lemma OAI.TamingCompatibility.MetricWedgePairing.formEquiv_volume line 140
14. lemma OAI.TamingCompatibility.MetricWedgePairing.formEquiv_wedgeTwo line 144
15. lemma OAI.TamingCompatibility.MetricWedgePairing.formEquiv_wedgeOne line 148
16. lemma OAI.TamingCompatibility.MetricWedgePairing.wedgeTwo_star line 159
17. lemma OAI.TamingCompatibility.MetricWedgePairing.wedgeOne_three line 166