OAI/Geometry/CylinderCovering/Ruled/CellCost.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ProductCells.translated_frame_area line 10
  2. lemma OAI.ProductCells.coordinate_parameter_area_pos line 23
  3. lemma OAI.ProductCells.framed_intercept_area line 29
  4. lemma OAI.ProductCells.framed_parameter_isCompact line 42
  5. lemma OAI.ProductCells.framed_intercept_isOpen line 48
  6. lemma OAI.ProductCells.framed_intercept_isBounded line 60
  7. lemma OAI.ProductCells.framed_productCylinder_openBounded line 70
  8. lemma OAI.ProductCells.framed_productCylinder_cost line 81
  9. lemma OAI.ProductCells.uniform_weight_comparison line 121
  10. lemma OAI.ProductCells.uniform_physicalWeight_comparison line 142
  11. def OAI.ProductCells.scaledCoordinateFrame line 152
  12. lemma OAI.ProductCells.scaledCoordinateFrame_image line 158
  13. lemma OAI.ProductCells.pair_frame_intercept_area line 166
  14. lemma OAI.ProductCells.pair_frame_parameter_isCompact line 176
  15. lemma OAI.ProductCells.pair_frame_productCylinder_openBounded line 181
  16. lemma OAI.ProductCells.pair_frame_productCylinder_cost line 190