OAI/Geometry/CAT0Fillings/Charts/Straightening.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CAT0Fillings.EuclideanStraightening.replaceMap line 33
  2. lemma OAI.CAT0Fillings.EuclideanStraightening.replaceMap_apply line 36
  3. lemma OAI.CAT0Fillings.EuclideanStraightening.replaceMap_lipschitz line 44
  4. lemma OAI.CAT0Fillings.EuclideanStraightening.det_updateRow_one line 68
  5. lemma OAI.CAT0Fillings.EuclideanStraightening.replaceMap_hasFDerivAt line 76
  6. lemma OAI.CAT0Fillings.EuclideanStraightening.det_replaceMap_fderiv line 82
  7. def OAI.CAT0Fillings.EuclideanStraightening.switchZero line 101
  8. lemma OAI.CAT0Fillings.EuclideanStraightening.switchZero_apply_zero line 104
  9. def OAI.CAT0Fillings.EuclideanStraightening.straightenMap line 108
  10. lemma OAI.CAT0Fillings.EuclideanStraightening.straightenMap_zero line 111
  11. lemma OAI.CAT0Fillings.EuclideanStraightening.straightenMap_lipschitz line 114