OAI/Geometry/CylinderCovering/Ruled/Similarity.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RuledApproximation.AxisPlane line 12
  2. def OAI.RuledApproximation.similarityPlaneEquiv line 14
  3. def OAI.RuledApproximation.similarityPlaneTranslation line 31
  4. def OAI.RuledApproximation.similarityPlaneMap line 36
  5. lemma OAI.RuledApproximation.similarityPlaneMap_coe line 44
  6. lemma OAI.RuledApproximation.similarityPlaneMap_image line 49
  7. lemma OAI.RuledApproximation.similarityPlane_finrank line 56
  8. lemma OAI.RuledApproximation.similarityPlane_area line 64
  9. lemma OAI.RuledApproximation.affineEquiv_combination line 73
  10. lemma OAI.RuledApproximation.IsParallelogram.affineEquiv line 80
  11. lemma OAI.RuledApproximation.IsTriangle.affineEquiv line 98
  12. def OAI.RuledApproximation.Cylinder.similarity line 118
  13. lemma OAI.RuledApproximation.Cylinder.carrier_eq_ambient line 124
  14. lemma OAI.RuledApproximation.Cylinder.similarity_carrier line 133
  15. lemma OAI.RuledApproximation.Cylinder.similarity_area line 141
  16. lemma OAI.RuledApproximation.Cylinder.similarity_parallelogram line 151
  17. lemma OAI.RuledApproximation.Cylinder.similarity_triangle line 156
  18. lemma OAI.RuledApproximation.Cylinder.similarity_openBounded line 161
  19. lemma OAI.RuledApproximation.similarity_familySet line 173
  20. lemma OAI.RuledApproximation.similarity_familyArea line 179
  21. lemma OAI.RuledApproximation.similarity_cover line 184
  22. lemma OAI.RuledApproximation.similarity_relativeCost line 192
  23. lemma OAI.RuledApproximation.HasFiniteCover.parallelogram_similarity line 207
  24. lemma OAI.RuledApproximation.HasFiniteCover.openBounded_similarity line 219
  25. lemma OAI.RuledApproximation.relativeCost_le_familyArea_div_minimum line 231
  26. lemma OAI.RuledApproximation.relativeCost_lt_half_of_familyArea_lt line 243
  27. lemma OAI.RuledApproximation.similarity_strict_total line 252