OAI/Geometry/CylinderCovering/Convexity/CylinderSimilarity.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CylinderCovering.Similarity.map_injective line 13
  2. lemma OAI.CylinderCovering.Similarity.map_surjective line 19
  3. lemma OAI.CylinderCovering.Similarity.map_continuous line 25
  4. lemma OAI.CylinderCovering.Similarity.project_map line 29
  5. lemma OAI.CylinderCovering.Similarity.project_perpendicular line 36
  6. lemma OAI.CylinderCovering.Similarity.transportedBase_perpendicular line 43
  7. lemma OAI.CylinderCovering.Similarity.carrier_image line 52
  8. lemma OAI.CylinderCovering.Similarity.covers_image line 69
  9. lemma OAI.CylinderCovering.Similarity.affineMap_apply line 80
  10. lemma OAI.CylinderCovering.Similarity.transportedBase_convex line 83
  11. lemma OAI.CylinderCovering.Similarity.transportedBase_triangular line 88
  12. lemma OAI.CylinderCovering.Similarity.euclideanHausdorffMeasure_map line 102
  13. lemma OAI.CylinderCovering.Similarity.area_map line 117
  14. lemma OAI.CylinderCovering.Similarity.area_transportedBase line 125
  15. lemma OAI.CylinderCovering.Similarity.transportedBase_compact line 131
  16. lemma OAI.CylinderCovering.Similarity.transportedBase_finite line 136
  17. lemma OAI.CylinderCovering.Similarity.shadowArea_map line 145
  18. lemma OAI.CylinderCovering.Similarity.shadowArea_range_map line 157
  19. lemma OAI.CylinderCovering.Similarity.minimumArea_le_shadowArea line 169
  20. lemma OAI.CylinderCovering.Similarity.minimumArea_map line 177
  21. lemma OAI.CylinderCovering.Similarity.areaRatio_map line 191