OAI/Geometry/CylinderCovering/Angular/Construction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TriangularCovering.lowerIntercept_eq_convexHull line 11
  2. theorem OAI.TriangularCovering.upperIntercept_eq_convexHull line 32
  3. theorem OAI.TriangularCovering.projectedCylinder_carrier_direction line 53
  4. theorem OAI.TriangularCovering.lowerCylinder_carrier_intercept line 72
  5. theorem OAI.TriangularCovering.upperCylinder_carrier_intercept line 80
  6. theorem OAI.TriangularCovering.lowerAngularBase_eq_projection_intercept line 88
  7. theorem OAI.TriangularCovering.upperAngularBase_eq_projection_intercept line 97
  8. theorem OAI.TriangularCovering.TriCylinder.ext_axis_base line 106
  9. theorem OAI.TriangularCovering.finiteFamily_explicit_laws line 114
  10. theorem OAI.TriangularCovering.ExplicitAngularFamily.unique line 121
  11. theorem OAI.TriangularCovering.ExplicitAngularFamily.eq_finiteFamily line 136
  12. theorem OAI.TriangularCovering.ExplicitAngularFamily.exact_area_sum line 140
  13. theorem OAI.TriangularCovering.ExplicitAngularFamily.covers line 147