OAI/Geometry/CylinderCovering/Ruled/CellCoordinates.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ProductCells.coordinateEquiv_apply_zero line 10
  2. lemma OAI.ProductCells.coordinateEquiv_apply_one line 11
  3. lemma OAI.ProductCells.coordinateEquiv_symm_apply line 12
  4. lemma OAI.ProductCells.coordinateEquiv_measurePreserving line 15
  5. lemma OAI.ProductCells.coordinate_image_volume line 18
  6. lemma OAI.ProductCells.coordinate_image_area line 26
  7. lemma OAI.ProductCells.mem_coordinateParameterCell line 30
  8. lemma OAI.ProductCells.mem_coordinateInterceptCell line 36
  9. lemma OAI.ProductCells.coordinateParameterCell_isCompact line 43
  10. lemma OAI.ProductCells.coordinateInterceptCell_isOpen line 46
  11. lemma OAI.ProductCells.coordinateInterceptCell_isBounded line 49
  12. lemma OAI.ProductCells.coordinate_parameter_area line 53
  13. lemma OAI.ProductCells.coordinate_intercept_area line 58
  14. lemma OAI.ProductCells.coordinate_area_ratio line 68
  15. lemma OAI.ProductCells.expanded_coordinateParameterCell_mem_intercept line 76