OAI/Geometry/CylinderCovering/Rational/EqualityCover.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SlopeRational.EqualityCover.tip line 14
  2. def OAI.SlopeRational.EqualityCover.left line 15
  3. def OAI.SlopeRational.EqualityCover.right line 16
  4. lemma OAI.SlopeRational.EqualityCover.firstAxis_unit line 18
  5. lemma OAI.SlopeRational.EqualityCover.first_triple line 24
  6. lemma OAI.SlopeRational.EqualityCover.first_triple_ne line 30
  7. def OAI.SlopeRational.EqualityCover.firstCylinder line 35
  8. def OAI.SlopeRational.EqualityCover.secondCylinder line 38
  9. lemma OAI.SlopeRational.EqualityCover.triangle_mem_iff line 41
  10. lemma OAI.SlopeRational.EqualityCover.firstBase_perpendicular line 64
  11. lemma OAI.SlopeRational.EqualityCover.firstCylinder_axis line 69
  12. lemma OAI.SlopeRational.EqualityCover.firstCylinder_base line 71
  13. lemma OAI.SlopeRational.EqualityCover.secondCylinder_axis line 82
  14. lemma OAI.SlopeRational.EqualityCover.secondCylinder_base line 86
  15. lemma OAI.SlopeRational.EqualityCover.secondBase_eq_label_image line 96
  16. lemma OAI.SlopeRational.EqualityCover.firstCylinder_area line 105
  17. lemma OAI.SlopeRational.EqualityCover.secondCylinder_area line 110
  18. lemma OAI.SlopeRational.EqualityCover.firstCylinder_covers_nonnegative line 114
  19. lemma OAI.SlopeRational.EqualityCover.reflection_mem_reference line 129
  20. lemma OAI.SlopeRational.EqualityCover.secondCylinder_covers_nonpositive line 141
  21. def OAI.SlopeRational.EqualityCover.cylinders line 152
  22. lemma OAI.SlopeRational.EqualityCover.cylinders_covers line 154
  23. lemma OAI.SlopeRational.EqualityCover.cylinders_area_each line 160
  24. lemma OAI.SlopeRational.EqualityCover.cylinders_totalArea line 165
  25. lemma OAI.SlopeRational.EqualityCover.secondAxis_unit line 170
  26. lemma OAI.SlopeRational.EqualityCover.centered_shadow line 174
  27. lemma OAI.SlopeRational.EqualityCover.firstAxis_shadow line 181
  28. lemma OAI.SlopeRational.EqualityCover.secondAxis_shadow line 190
  29. lemma OAI.SlopeRational.EqualityCover.cylinders_shadow_each line 199
  30. lemma OAI.SlopeRational.EqualityCover.cylinders_relativeCost line 208
  31. theorem OAI.SlopeRational.EqualityCover.equality_cover line 216