OAI/Geometry/CylinderCovering/Caps/FiniteArea.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CylinderCovering.HalfheightFinite.normalFirst line 14
  2. def OAI.CylinderCovering.HalfheightFinite.normalSecond line 15
  3. def OAI.CylinderCovering.HalfheightFinite.radialFirst line 16
  4. def OAI.CylinderCovering.HalfheightFinite.radialSecond line 17
  5. def OAI.CylinderCovering.HalfheightFinite.transverseFirst line 18
  6. def OAI.CylinderCovering.HalfheightFinite.transverseSecond line 19
  7. def OAI.CylinderCovering.HalfheightFinite.originSecond line 20
  8. def OAI.CylinderCovering.HalfheightFinite.velocityFirst line 21
  9. def OAI.CylinderCovering.HalfheightFinite.velocitySecond line 22
  10. lemma OAI.CylinderCovering.HalfheightFinite.height_positive line 24
  11. lemma OAI.CylinderCovering.HalfheightFinite.height_squared line 25
  12. lemma OAI.CylinderCovering.HalfheightFinite.normalFirst_unit line 27
  13. lemma OAI.CylinderCovering.HalfheightFinite.normalSecond_unit line 30
  14. lemma OAI.CylinderCovering.HalfheightFinite.first_chart line 34
  15. lemma OAI.CylinderCovering.HalfheightFinite.second_chart line 39
  16. lemma OAI.CylinderCovering.HalfheightFinite.first_raw line 45
  17. lemma OAI.CylinderCovering.HalfheightFinite.second_raw line 48
  18. lemma OAI.CylinderCovering.HalfheightFinite.first_gram line 52
  19. lemma OAI.CylinderCovering.HalfheightFinite.second_gram line 61
  20. lemma OAI.CylinderCovering.HalfheightFinite.velocityFirst_norm_sq line 71
  21. lemma OAI.CylinderCovering.HalfheightFinite.velocitySecond_norm_sq line 76
  22. theorem OAI.CylinderCovering.HalfheightFinite.firstFoot_projection_area line 82
  23. theorem OAI.CylinderCovering.HalfheightFinite.secondFoot_projection_area line 93
  24. theorem OAI.CylinderCovering.HalfheightFinite.firstFoot_projection_finite line 104
  25. theorem OAI.CylinderCovering.HalfheightFinite.secondFoot_projection_finite line 115
  26. theorem OAI.CylinderCovering.HalfheightFinite.firstBase_area line 126
  27. theorem OAI.CylinderCovering.HalfheightFinite.secondBase_area line 136
  28. theorem OAI.CylinderCovering.HalfheightFinite.totalArea_eq_two_sum line 146