OAI/Geometry/CylinderCovering/Caps/FiniteShapes.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.HalfheightFinite.shape_height_pos line 14
  2. theorem OAI.CylinderCovering.HalfheightFinite.shape_ex_norm line 16
  3. theorem OAI.CylinderCovering.HalfheightFinite.shape_ey_norm line 19
  4. theorem OAI.CylinderCovering.HalfheightFinite.shape_first_independent line 22
  5. theorem OAI.CylinderCovering.HalfheightFinite.shape_second_independent line 34
  6. def OAI.CylinderCovering.HalfheightFinite.firstShapeChart line 46
  7. def OAI.CylinderCovering.HalfheightFinite.secondShapeChart line 50
  8. theorem OAI.CylinderCovering.HalfheightFinite.firstShapeChart_apply line 54
  9. theorem OAI.CylinderCovering.HalfheightFinite.secondShapeChart_apply line 62
  10. theorem OAI.CylinderCovering.HalfheightFinite.firstShapeChart_injective line 70
  11. theorem OAI.CylinderCovering.HalfheightFinite.secondShapeChart_injective line 84
  12. theorem OAI.CylinderCovering.HalfheightFinite.firstBase_eq_shapeChart line 98
  13. theorem OAI.CylinderCovering.HalfheightFinite.secondBase_eq_shapeChart line 102
  14. theorem OAI.CylinderCovering.HalfheightFinite.finite_base_trapezoids line 106
  15. theorem OAI.CylinderCovering.HalfheightFinite.cubic_maxCap_nonneg line 129
  16. theorem OAI.CylinderCovering.HalfheightFinite.fractional_maxCap_nonneg line 139
  17. theorem OAI.CylinderCovering.HalfheightFinite.source_base_trapezoids line 149