OAI/Geometry/ProjectionVolume/PolytopeFront.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Paper092.HPolytope.slack line 18
  2. def OAI.Paper092.HPolytope.velocity line 20
  3. theorem OAI.Paper092.HPolytope.slack_add_smul line 22
  4. theorem OAI.Paper092.HPolytope.mem_body_iff_slack line 27
  5. theorem OAI.Paper092.HPolytope.mem_face_iff_slack line 31
  6. theorem OAI.Paper092.HPolytope.body_nonempty line 40
  7. theorem OAI.Paper092.HPolytope.body_convex line 44
  8. theorem OAI.Paper092.HPolytope.velocity_neg_exists line 55
  9. theorem OAI.Paper092.HPolytope.exists_front_point line 72
  10. theorem OAI.Paper092.HPolytope.projection_injective_on_front line 83
  11. theorem OAI.Paper092.HPolytope.projection_eq_front_cover line 106
  12. theorem OAI.Paper092.HPolytope.front_faces_projection_inter_eq line 121
  13. def OAI.Paper092.HPolytope.slackAffine line 136
  14. theorem OAI.Paper092.HPolytope.slackAffine_apply line 139
  15. theorem OAI.Paper092.HPolytope.seam_projection_invariant line 141
  16. theorem OAI.Paper092.HPolytope.index_eq_of_weighted_slack_zero line 152
  17. theorem OAI.Paper092.HPolytope.projected_seam_null line 175
  18. theorem OAI.Paper092.HPolytope.projected_front_faces_aedisjoint line 204
  19. theorem OAI.Paper092.HPolytope.face_isCompact line 218
  20. theorem OAI.Paper092.HPolytope.projected_face_isCompact line 221
  21. theorem OAI.Paper092.HPolytope.projectionVolume_eq_front_sum line 225
  22. theorem OAI.Paper092.HPolytope.brightness_eq_front_sum line 243
  23. theorem OAI.Paper092.HPolytope.face_brightness line 253