OAI/Geometry/CylinderCovering/Footprints/QuadraticPhysicalFootprints.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CylinderCovering.Footprints.physicalPairEquiv line 14
  2. theorem OAI.CylinderCovering.Footprints.physicalPairEquiv_apply line 18
  3. theorem OAI.CylinderCovering.Footprints.physicalPair_measurePreserving line 21
  4. def OAI.CylinderCovering.Footprints.physicalChartEquiv line 27
  5. theorem OAI.CylinderCovering.Footprints.physicalChartEquiv_apply line 30
  6. theorem OAI.CylinderCovering.Footprints.physicalChart_measurePreserving line 33
  7. theorem OAI.CylinderCovering.Footprints.physicalLabelSet_volume line 36
  8. theorem OAI.CylinderCovering.Footprints.physicalLabelSet_realVolume line 45
  9. theorem OAI.CylinderCovering.Footprints.physicalChart_continuous line 49
  10. theorem OAI.CylinderCovering.Footprints.physicalLabelSet_compact line 53
  11. theorem OAI.CylinderCovering.Footprints.projected_footprint_area line 56
  12. theorem OAI.CylinderCovering.Footprints.quadraticSweepPoint_mem_projected line 68
  13. def OAI.CylinderCovering.Footprints.physicalChartAffine line 80
  14. def OAI.CylinderCovering.Footprints.projectedFootprintChart line 92
  15. theorem OAI.CylinderCovering.Footprints.projectedFootprintChart_injective line 98
  16. theorem OAI.CylinderCovering.Footprints.projected_footprint_base line 102
  17. theorem OAI.CylinderCovering.Footprints.projected_footprint_compact line 110
  18. theorem OAI.CylinderCovering.Footprints.projected_footprint_convex line 118
  19. theorem OAI.CylinderCovering.Footprints.projected_affine_triangle line 124
  20. theorem OAI.CylinderCovering.Footprints.projected_footprint_area_sqrtTwo line 138
  21. theorem OAI.CylinderCovering.Footprints.projected_footprint_convex_iff line 146
  22. theorem OAI.CylinderCovering.Footprints.projected_footprint_ambient_base line 157
  23. theorem OAI.CylinderCovering.Footprints.physicalFootprintRealization line 165
  24. theorem OAI.CylinderCovering.Footprints.physicalFootprintCertificates line 176
  25. theorem OAI.CylinderCovering.Footprints.quadratic_footprintCylinder_eq line 179
  26. theorem OAI.CylinderCovering.Footprints.physical_absolute_contains line 183
  27. theorem OAI.CylinderCovering.Footprints.physical_midpoint_absolute_contains line 193
  28. theorem OAI.CylinderCovering.Footprints.physical_midpoint_affine_contains line 203
  29. theorem OAI.CylinderCovering.Footprints.physical_endpoint_contains line 213