OAI/Geometry/BallPacking/Necessity/LocalCharts.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HigherDimensionalBallPacking.Rigidity.affineC1Value line 46
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.affineC1Value_apply line 53
  3. def OAI.HigherDimensionalBallPacking.Rigidity.affineC1Deriv line 58
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.affineC1Deriv_apply line 64
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1HolderCRFamily_fderiv line 70
  6. def OAI.HigherDimensionalBallPacking.Rigidity.markedFramedCR line 106
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.markedFramedCR_contDiffAt_zero line 115
  8. lemma OAI.HigherDimensionalBallPacking.Rigidity.affineC1Curve_profile line 131
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.markedFramedCR_fderiv_zero line 140
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.affineC1_uniform_exterior line 184
  11. lemma OAI.HigherDimensionalBallPacking.Rigidity.affineC1Curve_add line 225
  12. lemma OAI.HigherDimensionalBallPacking.Rigidity.framed_variation_exterior_cr line 236
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.markedFramedCR_eventually_compact line 262
  14. lemma OAI.HigherDimensionalBallPacking.Rigidity.linearIsometry_fderiv_mem line 332
  15. def OAI.HigherDimensionalBallPacking.Rigidity.reflectedFDeriv line 350
  16. lemma OAI.HigherDimensionalBallPacking.Rigidity.reflectedFDeriv_comp line 355
  17. lemma OAI.HigherDimensionalBallPacking.Rigidity.hasFDerivAt_reflected line 361
  18. lemma OAI.HigherDimensionalBallPacking.Rigidity.fderiv_comp_linearIsometry line 371
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.contDiffAt_reflect_isometry_nat line 383
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.contDiffAt_reflect_isometry line 410
  21. def OAI.HigherDimensionalBallPacking.Rigidity.localCodRestrict line 426
  22. lemma OAI.HigherDimensionalBallPacking.Rigidity.localCodRestrict_eq line 431
  23. lemma OAI.HigherDimensionalBallPacking.Rigidity.localCodRestrict_eventually line 436
  24. def OAI.HigherDimensionalBallPacking.Rigidity.submoduleInclusionIsometry line 442
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.localCodRestrict_contDiffAt line 446
  26. theorem OAI.HigherDimensionalBallPacking.Rigidity.localCodRestrict_fderiv line 453
  27. def OAI.HigherDimensionalBallPacking.Rigidity.compactMarkedCR line 479
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactMarkedCR_local_chart line 491