OAI/Geometry/CylinderCovering/Nilpotent/ApexNet.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CylinderCovering.NilpotentApexNet.meshCount_pos line 10
  2. lemma OAI.CylinderCovering.NilpotentApexNet.step_le line 13
  3. lemma OAI.CylinderCovering.NilpotentApexNet.count_bound line 21
  4. lemma OAI.CylinderCovering.NilpotentApexNet.first_crossing line 30
  5. lemma OAI.CylinderCovering.NilpotentApexNet.node_bounds line 45
  6. lemma OAI.CylinderCovering.NilpotentApexNet.exists_near_node line 58
  7. lemma OAI.CylinderCovering.NilpotentApexNet.v_lipschitz line 79
  8. lemma OAI.CylinderCovering.NilpotentApexNet.velocity_difference line 87
  9. lemma OAI.CylinderCovering.NilpotentApexNet.residual_bound line 111
  10. theorem OAI.CylinderCovering.NilpotentApexNet.apex_cover line 140
  11. lemma OAI.CylinderCovering.NilpotentApexNet.weight_bounds line 147
  12. lemma OAI.CylinderCovering.NilpotentApexNet.tile_area line 153
  13. theorem OAI.CylinderCovering.NilpotentApexNet.apex_cost line 164
  14. lemma OAI.CylinderCovering.NilpotentApexNet.tile_compact line 182
  15. lemma OAI.CylinderCovering.NilpotentApexNet.tile_convex line 184
  16. lemma OAI.CylinderCovering.NilpotentApexNet.tile_measurable line 186
  17. lemma OAI.CylinderCovering.NilpotentApexNet.radius_pos line 188
  18. lemma OAI.CylinderCovering.NilpotentApexNet.tile_area_pos line 192
  19. theorem OAI.CylinderCovering.NilpotentApexNet.apexNet line 197
  20. theorem OAI.CylinderCovering.NilpotentApexNet.auxiliaryApexNet line 213