OAI/Geometry/IntegralFillings/Charts/Straightening.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpIntegralFillings.EuclideanStraightening.replaceMap line 33
2. lemma OAI.SharpIntegralFillings.EuclideanStraightening.replaceMap_apply line 36
3. lemma OAI.SharpIntegralFillings.EuclideanStraightening.replaceMap_lipschitz line 44
4. lemma OAI.SharpIntegralFillings.EuclideanStraightening.det_updateRow_one line 70
5. lemma OAI.SharpIntegralFillings.EuclideanStraightening.replaceMap_hasFDerivAt line 78
6. lemma OAI.SharpIntegralFillings.EuclideanStraightening.det_replaceMap_fderiv line 84
7. def OAI.SharpIntegralFillings.EuclideanStraightening.switchZero line 103
8. lemma OAI.SharpIntegralFillings.EuclideanStraightening.switchZero_apply_zero line 106
9. def OAI.SharpIntegralFillings.EuclideanStraightening.straightenMap line 110
10. lemma OAI.SharpIntegralFillings.EuclideanStraightening.straightenMap_zero line 113
11. lemma OAI.SharpIntegralFillings.EuclideanStraightening.straightenMap_lipschitz line 116