OAI/Geometry/TamingCompatibility/DifferentialForms/WedgeTransform.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.UnitaryFrame.wedgeTransform line 13
2. lemma OAI.TamingCompatibility.UnitaryFrame.wedgeTransform_apply line 17
3. lemma OAI.TamingCompatibility.UnitaryFrame.wedgeTransform_wedge line 21
4. lemma OAI.TamingCompatibility.UnitaryFrame.wedge_smul_left line 28
5. lemma OAI.TamingCompatibility.UnitaryFrame.wedge_smul_right line 32
6. lemma OAI.TamingCompatibility.UnitaryFrame.wedge_sub_right line 36
7. lemma OAI.TamingCompatibility.UnitaryFrame.wedge_self line 40
8. lemma OAI.TamingCompatibility.UnitaryFrame.norm_wedge_orthonormal line 44
9. lemma OAI.TamingCompatibility.UnitaryFrame.wedge_normalized line 51
10. lemma OAI.TamingCompatibility.UnitaryFrame.norm_wedge_area line 58
11. lemma OAI.TamingCompatibility.UnitaryFrame.wedge_contDiff line 66
12. lemma OAI.TamingCompatibility.UnitaryFrame.wedgeTransform_contDiff line 75
13. lemma OAI.TamingCompatibility.PlaneVariation.first_lipschitz_bound line 87