OAI/Geometry/BallPacking/Degree/ChartFormZeroExtension.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.supported_indicator_smooth line 14
  2. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.extDeriv_supported_indicator line 31
  3. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.supporting_chart_compact line 56
  4. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.supporting_chart_zero line 61
  5. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.chartExtension line 66
  6. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.chartExtension_zero line 70
  7. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.chartExtension_smooth line 78
  8. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.chartExtension_support line 87
  9. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.exterior_chartExtension line 92
  10. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.chartMass line 101
  11. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.chart_coefficient_integrable line 104
  12. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.chartMass_exterior_zero line 117
  13. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.chartMass_eq_compact_integral line 134
  14. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.chartMass_change line 149
  15. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.chartMass_sum line 167
  16. structure OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasPartition line 186
  17. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasPartition.mass line 195
  18. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasPartition.smul_sum line 199
  19. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasPartition.mass_eq_chartMass line 208
  20. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasPartition.mass_sum line 238
  21. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.extDeriv_fintype_sum line 258
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasPartition.compact_stokes line 266
  23. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.alternationCLM line 304
  24. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.alternationCLM_alternating line 324
  25. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.contDiffOn_alternating_of_multilinear line 333
  26. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.contDiffOn_alternating_comp line 342
  27. structure OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasSmoothMap line 364
  28. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasSmoothMap.derivative_transition line 371
  29. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasSmoothMap.pullback line 386
  30. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasSmoothMap.pullback_exterior line 399
  31. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasSmoothMap.pullback_supported line 409
  32. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.spatialBox line 424
  33. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.lowerCorner line 425
  34. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.upperCorner line 426
  35. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.exitFaces line 428
  36. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.corners_le line 432
  37. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.exitFaces_compact line 438
  38. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.tail_mem_spatialBox line 445
  39. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.time_mem_interval line 449
  40. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.timeFace_mem_box line 453
  41. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.initialFace_box line 462
  42. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.insertNth_mem_box line 467
  43. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.sideFace_mem_exit line 478
  44. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.norm_ball_subset_spatialBox line 495
  45. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.separating_bump line 504
  46. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.bump_initial_integral_pos line 521