OAI/Geometry/CylinderCovering/Angular/GeneralGeometry.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CylinderCovering.AngularGeneral.planarSector_eq_image line 13
  2. lemma OAI.CylinderCovering.AngularGeneral.planarSector_compact line 23
  3. lemma OAI.CylinderCovering.AngularGeneral.lowerAxis_eq_physicalUnit line 31
  4. lemma OAI.CylinderCovering.AngularGeneral.lowerAxis_norm line 35
  5. lemma OAI.CylinderCovering.AngularGeneral.lowerIntercept_eq_image line 39
  6. lemma OAI.CylinderCovering.AngularGeneral.projection_physicalUnit line 48
  7. lemma OAI.CylinderCovering.AngularGeneral.lowerBase_eq_rawImage line 58
  8. lemma OAI.CylinderCovering.AngularGeneral.ambient_area_of_intrinsic line 66
  9. lemma OAI.CylinderCovering.AngularGeneral.lowerBase_area line 79
  10. lemma OAI.CylinderCovering.AngularGeneral.lowerBase_compact line 97
  11. lemma OAI.CylinderCovering.AngularGeneral.lowerBase_finite line 103
  12. lemma OAI.CylinderCovering.AngularGeneral.projection_add line 115
  13. lemma OAI.CylinderCovering.AngularGeneral.projection_rotate line 122
  14. lemma OAI.CylinderCovering.AngularGeneral.upperDirection_eq_rotate line 127
  15. lemma OAI.CylinderCovering.AngularGeneral.upperAxis_eq_rotate line 133
  16. lemma OAI.CylinderCovering.AngularGeneral.upperAxis_norm line 138
  17. lemma OAI.CylinderCovering.AngularGeneral.upperIntercept_eq_image line 141
  18. lemma OAI.CylinderCovering.AngularGeneral.upperBase_eq_image line 155
  19. lemma OAI.CylinderCovering.AngularGeneral.upperBase_area_eq_lower line 164
  20. lemma OAI.CylinderCovering.AngularGeneral.upperBase_area line 173
  21. lemma OAI.CylinderCovering.AngularGeneral.upperBase_compact line 180
  22. lemma OAI.CylinderCovering.AngularGeneral.upperBase_finite line 186
  23. lemma OAI.CylinderCovering.AngularGeneral.projected_base_perpendicular line 196
  24. lemma OAI.CylinderCovering.AngularGeneral.base_properties line 202
  25. lemma OAI.CylinderCovering.AngularGeneral.totalArea_eq_planar_sum line 215
  26. lemma OAI.CylinderCovering.AngularGeneral.cell_cost_of_planar_volume line 222
  27. lemma OAI.CylinderCovering.AngularGeneral.integral_cost_of_planar_volumes line 239