OAI/Geometry/ProjectionVolume/CubeBrightness.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Paper092.euclideanCube line 14
  2. theorem OAI.Paper092.mem_euclideanCube line 17
  3. theorem OAI.Paper092.euclideanCube_isCompact line 25
  4. theorem OAI.Paper092.euclideanCube_volume line 28
  5. def OAI.Paper092.cubeNormal line 32
  6. def OAI.Paper092.cubeOffset line 36
  7. theorem OAI.Paper092.cube_constraints line 40
  8. def OAI.Paper092.cubePolytope line 46
  9. theorem OAI.Paper092.cubePolytope_body line 71
  10. theorem OAI.Paper092.cubePolytope_face_lower line 74
  11. theorem OAI.Paper092.cubePolytope_face_upper line 81
  12. theorem OAI.Paper092.cube_lower_face_chart line 88
  13. theorem OAI.Paper092.cube_lower_face_area line 104
  14. theorem OAI.Paper092.cube_upper_face_eq_vadd line 112
  15. theorem OAI.Paper092.cube_upper_face_area line 143
  16. theorem OAI.Paper092.cube_faceArea line 147
  17. theorem OAI.Paper092.euclideanCube_brightness line 158
  18. theorem OAI.Paper092.euclideanCube_diagonal_brightness line 166
  19. theorem OAI.Paper092.euclideanCube_diagonal_extrusion line 171
  20. theorem OAI.Paper092.euclideanCube_diagonal_projectionBody_support line 181