OAI/Geometry/ProjectionVolume/ProductProjection.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Paper092.ProductFacetIndex line 11
  2. def OAI.Paper092.productCoordinates line 13
  3. def OAI.Paper092.productVelocity line 17
  4. theorem OAI.Paper092.productCoordinates_add_smul line 21
  5. theorem OAI.Paper092.mem_productWitness_iff_coordinates line 27
  6. theorem OAI.Paper092.productVelocity_neg_exists line 39
  7. theorem OAI.Paper092.exists_product_front_point line 54
  8. theorem OAI.Paper092.projection_injective_on_product_front line 65
  9. def OAI.Paper092.productFacet line 87
  10. theorem OAI.Paper092.product_projection_eq_front_cover line 90
  11. theorem OAI.Paper092.product_front_facets_projection_inter_eq line 106
  12. def OAI.Paper092.productCoordinateAffine line 122
  13. theorem OAI.Paper092.productCoordinateAffine_apply line 128
  14. def OAI.Paper092.productVertex line 134
  15. theorem OAI.Paper092.firstBlock_productVertex line 137
  16. theorem OAI.Paper092.secondBlock_productVertex line 142
  17. theorem OAI.Paper092.exists_product_coordinate_separator line 147
  18. theorem OAI.Paper092.product_facet_seam_projection_invariant line 171
  19. theorem OAI.Paper092.projected_product_facet_seam_null line 186
  20. theorem OAI.Paper092.projected_product_front_facets_aedisjoint line 220
  21. theorem OAI.Paper092.productFacet_isCompact line 236
  22. theorem OAI.Paper092.projected_productFacet_isCompact line 245
  23. theorem OAI.Paper092.projectionVolume_product_eq_front_sum line 249
  24. theorem OAI.Paper092.brightness_product_eq_front_sum line 266