OAI/Geometry/TamingCompatibility/DifferentialForms/UnitaryVectors.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.SmoothMetric.exists_unitary_vectors line 30
2. lemma OAI.TamingCompatibility.SmoothMetric.exists_orthonormalFrame_near line 46
3. lemma OAI.TamingCompatibility.SmoothMetric.contDiffOn_pairing_two_frame line 67
4. lemma OAI.TamingCompatibility.SmoothMetric.contDiffOn_pairing_three_frame line 81
5. lemma OAI.TamingCompatibility.SmoothMetric.contDiffOn_pairing_two line 95
6. lemma OAI.TamingCompatibility.SmoothMetric.contDiffOn_pairing_three line 108
7. lemma OAI.TamingCompatibility.SmoothHodge.volumeSquare_contDiffOn line 129
8. lemma OAI.TamingCompatibility.SmoothHodge.curryLeft_contDiffOn line 146
9. lemma OAI.TamingCompatibility.SmoothHodge.comp_contDiffOn line 152
10. lemma OAI.TamingCompatibility.SmoothHodge.starTwo_contDiffOn line 168
11. lemma OAI.TamingCompatibility.SmoothHodge.starThree_contDiffOn line 173