OAI/Geometry/CylinderCovering/Angular/Geometry.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AngularGeometry.lowerCylinder line 11
  2. def OAI.AngularGeometry.upperCylinder line 14
  3. lemma OAI.AngularGeometry.lowerCylinder_axis line 17
  4. lemma OAI.AngularGeometry.upperCylinder_axis line 21
  5. lemma OAI.AngularGeometry.lowerCylinder_carrier line 35
  6. lemma OAI.AngularGeometry.upperCylinder_carrier line 49
  7. lemma OAI.AngularGeometry.lowerCylinder_area line 64
  8. lemma OAI.AngularGeometry.upperCylinder_area line 74
  9. lemma OAI.AngularGeometry.lowerCylinder_compact line 79
  10. lemma OAI.AngularGeometry.upperCylinder_compact line 83
  11. lemma OAI.AngularGeometry.lowerCylinder_measurable_finite line 89
  12. lemma OAI.AngularGeometry.upperCylinder_measurable_finite line 95
  13. lemma OAI.AngularGeometry.pair_families line 101
  14. theorem OAI.AngularGeometry.paired_family line 125
  15. lemma OAI.AngularGeometry.areaFactor_sqrt_two line 146
  16. theorem OAI.AngularGeometry.paired_cover line 152