OAI/Geometry/CylinderCovering/Physical/PhysicalFootprints.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.PhysicalFootprints.footCoordinates_continuous line 13
  2. theorem OAI.CylinderCovering.PhysicalFootprints.footCoordinates_injective line 17
  3. def OAI.CylinderCovering.PhysicalFootprints.footCoordinatesLinear line 24
  4. def OAI.CylinderCovering.PhysicalFootprints.footCoordinatesAffine line 32
  5. def OAI.CylinderCovering.PhysicalFootprints.projectedFootAffine line 40
  6. theorem OAI.CylinderCovering.PhysicalFootprints.projectedFootAffine_apply line 43
  7. def OAI.CylinderCovering.PhysicalFootprints.perpendicularFootAffine line 46
  8. theorem OAI.CylinderCovering.PhysicalFootprints.perpendicularFootAffine_injective line 50
  9. theorem OAI.CylinderCovering.PhysicalFootprints.footCoordinates_measurePreserving line 54
  10. theorem OAI.CylinderCovering.PhysicalFootprints.footCoordinates_volume line 68
  11. theorem OAI.CylinderCovering.PhysicalFootprints.footCoordinates_volume_real line 75
  12. theorem OAI.CylinderCovering.PhysicalFootprints.projectedFoot_eq_rawProjection line 79
  13. theorem OAI.CylinderCovering.PhysicalFootprints.projectedFoot_injective line 82
  14. def OAI.CylinderCovering.PhysicalFootprints.footprintCylinder line 90
  15. theorem OAI.CylinderCovering.PhysicalFootprints.footprintCylinder_axis line 93
  16. theorem OAI.CylinderCovering.PhysicalFootprints.footprintCylinder_base line 96
  17. theorem OAI.CylinderCovering.PhysicalFootprints.footprintCylinder_base_image line 102
  18. theorem OAI.CylinderCovering.PhysicalFootprints.footprintCylinder_compact line 108
  19. theorem OAI.CylinderCovering.PhysicalFootprints.footprintCylinder_carrier line 113
  20. theorem OAI.CylinderCovering.PhysicalFootprints.footprintCylinder_area line 123
  21. theorem OAI.CylinderCovering.PhysicalFootprints.physical_footprints line 128
  22. theorem OAI.CylinderCovering.PhysicalFootprints.projectedFoot_convex_iff line 136
  23. theorem OAI.CylinderCovering.PhysicalFootprints.projectedFoot_affineIndependent_iff line 146
  24. theorem OAI.CylinderCovering.PhysicalFootprints.projectedFoot_convexHull line 151
  25. theorem OAI.CylinderCovering.PhysicalFootprints.projection_shapes line 155
  26. theorem OAI.CylinderCovering.PhysicalFootprints.footprintCylinder_triangle line 161
  27. theorem OAI.CylinderCovering.PhysicalFootprints.footprintCylinder_trapezoid line 174
  28. theorem OAI.CylinderCovering.PhysicalFootprints.footprintCylinder_convex_iff line 188