OAI/Geometry/CylinderCovering/Barycentric/Sector.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RadialCoordinates.BarycentricSector.ray_sum line 13
  2. theorem OAI.RadialCoordinates.BarycentricSector.mem_positiveSector_iff line 16
  3. theorem OAI.RadialCoordinates.BarycentricSector.positiveSector_convex line 43
  4. theorem OAI.RadialCoordinates.BarycentricSector.positiveSector_eq_convexHull line 56
  5. theorem OAI.RadialCoordinates.BarycentricSector.isCompact_positiveSector line 83
  6. theorem OAI.RadialCoordinates.BarycentricSector.signedSector_eq_union line 88
  7. theorem OAI.RadialCoordinates.BarycentricSector.signedSector_eq_two_triangles line 103
  8. theorem OAI.RadialCoordinates.BarycentricSector.isCompact_signedSector line 110
  9. theorem OAI.RadialCoordinates.BarycentricSector.positive_negative_inter line 117
  10. def OAI.RadialCoordinates.BarycentricSector.coordinateShear line 140
  11. theorem OAI.RadialCoordinates.BarycentricSector.coordinateShear_apply line 144
  12. theorem OAI.RadialCoordinates.BarycentricSector.coordinateShear_det line 149
  13. theorem OAI.RadialCoordinates.BarycentricSector.positiveSector_eq_radial_image line 153
  14. theorem OAI.RadialCoordinates.BarycentricSector.positiveSector_volume line 169
  15. theorem OAI.RadialCoordinates.BarycentricSector.signedSector_volume line 180
  16. theorem OAI.RadialCoordinates.BarycentricSector.signedSector_area line 196
  17. theorem OAI.RadialCoordinates.BarycentricSector.vertices_affineIndependent line 202
  18. theorem OAI.RadialCoordinates.BarycentricSector.ray_norm_le_one line 223
  19. theorem OAI.RadialCoordinates.BarycentricSector.ray_sub_norm line 229
  20. theorem OAI.RadialCoordinates.BarycentricSector.perimeter_eq line 236
  21. theorem OAI.RadialCoordinates.BarycentricSector.perimeter_le line 243
  22. theorem OAI.RadialCoordinates.BarycentricSector.collar_sector_area line 254
  23. theorem OAI.RadialCoordinates.BarycentricSector.collar_sector_area_error line 260
  24. theorem OAI.RadialCoordinates.BarycentricSector.collar_perimeters_le line 277
  25. theorem OAI.RadialCoordinates.BarycentricSector.frozen_intercept_mem_cthickening line 292