OAI/Geometry/CylinderCovering/Convexity/IsometricCylinderEmbedding.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CylinderCovering.IsometricEmbedding.map_isometry line 15
  2. lemma OAI.CylinderCovering.IsometricEmbedding.baseMap_isometry line 20
  3. lemma OAI.CylinderCovering.IsometricEmbedding.axis_unit line 23
  4. lemma OAI.CylinderCovering.IsometricEmbedding.project_map line 26
  5. lemma OAI.CylinderCovering.IsometricEmbedding.projected_image_eq line 33
  6. lemma OAI.CylinderCovering.IsometricEmbedding.carrier_image line 42
  7. lemma OAI.CylinderCovering.IsometricEmbedding.covers_image line 57
  8. lemma OAI.CylinderCovering.IsometricEmbedding.transportedBase_perpendicular line 68
  9. lemma OAI.CylinderCovering.IsometricEmbedding.transportedBase_compact line 78
  10. lemma OAI.CylinderCovering.IsometricEmbedding.projected_image_compact line 82
  11. lemma OAI.CylinderCovering.IsometricEmbedding.projected_image_perpendicular line 89
  12. lemma OAI.CylinderCovering.IsometricEmbedding.transportedBase_measure line 101
  13. lemma OAI.CylinderCovering.IsometricEmbedding.transportedBase_area line 107
  14. lemma OAI.CylinderCovering.IsometricEmbedding.projected_image_area line 112
  15. lemma OAI.CylinderCovering.IsometricEmbedding.transportedBase_finite line 117
  16. lemma OAI.CylinderCovering.IsometricEmbedding.actual_total_area line 123
  17. lemma OAI.CylinderCovering.IsometricEmbedding.actual_limsup_le line 131
  18. lemma OAI.CylinderCovering.IsometricEmbedding.scaled_map_image line 140
  19. lemma OAI.CylinderCovering.IsometricEmbedding.scaled_project_map line 147
  20. lemma OAI.CylinderCovering.IsometricEmbedding.scaled_projected_image_eq line 155
  21. lemma OAI.CylinderCovering.IsometricEmbedding.scaled_map_measure line 165
  22. lemma OAI.CylinderCovering.IsometricEmbedding.scaled_map_area line 172
  23. lemma OAI.CylinderCovering.IsometricEmbedding.scaled_transportedBase_area line 180
  24. lemma OAI.CylinderCovering.IsometricEmbedding.scaled_projected_image_area line 185
  25. lemma OAI.CylinderCovering.IsometricEmbedding.scaled_transportedBase_finite line 191
  26. lemma OAI.CylinderCovering.IsometricEmbedding.scaled_actual_total_area line 200
  27. lemma OAI.CylinderCovering.IsometricEmbedding.scaled_actual_eventually_le line 210
  28. lemma OAI.CylinderCovering.IsometricEmbedding.scaled_carrier_image line 227
  29. lemma OAI.CylinderCovering.IsometricEmbedding.scaled_actual_limsup_le line 246