OAI/Geometry/BallPacking/Necessity/TangentLimits.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.frame_rescale_inverse line 40
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.field_C0_C1At line 69
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.fderiv_translate line 200
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.locally_uniform_translate line 208
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.field_C0_C1_closure line 222
  6. def OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.tangentMap line 288
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.tangentMap_apply line 293
  8. def OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.shearEquiv line 297
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.HasFrame.square line 308
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.tangentMap_hasFrame line 314
  11. def OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.tangentField line 343
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.tangentField_smooth line 347
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.field_derivative_anticommute line 361
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.tangentField_hasFrame line 380
  15. def OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.tangentCurve line 399
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.tangentCurve_smooth line 402
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.fderiv_directional line 407
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.tangentCurve_fderiv line 414
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.tangentCurve_CR line 423
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.field_C1_CR_limit line 469
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.realLinear_complex_apply line 517
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.CR_contDiff_succ line 525
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.field_C0_contDiff_nat line 548
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.field_C0_smooth_closure line 586
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.frame_rescale_inverse line 612
  26. theorem OAI.HigherDimensionalBallPacking.Rigidity.PseudoHolomorphicAt_limit line 648
  27. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_C0_C1At line 685
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_C0_C1_CR line 802