OAI/Geometry/CylinderCovering/Radial/ZeroCapSeparation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_kappa line 11
  2. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_direction line 13
  3. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_scalarBound line 17
  4. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_radialError line 21
  5. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_collar line 24
  6. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_capMax line 27
  7. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_weightedArea line 32
  8. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_sweep line 35
  9. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_localSweep line 46
  10. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_actualBase line 58
  11. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_frozenArea line 72
  12. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_actualBase_area line 84
  13. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_actualCost line 92
  14. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_frozenArea_pos line 96
  15. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_frozenArea_sum line 104
  16. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_frozenBase_area line 114
  17. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_actualBase_ssubset line 122
  18. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_totalArea line 133
  19. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_actualCost_lt_totalArea line 142
  20. theorem OAI.CylinderCovering.RadialSweep.zeroCapData_totalArea_tendsto line 152