OAI/Geometry/CylinderCovering/Rational/TetrahedronVolume.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RationalTetrahedron.hpos line 12
  2. def OAI.RationalTetrahedron.tripleEquiv line 14
  3. theorem OAI.RationalTetrahedron.tripleEquiv_apply line 19
  4. theorem OAI.RationalTetrahedron.tripleEquiv_measurePreserving line 24
  5. theorem OAI.RationalTetrahedron.mem_tetrahedron_iff line 30
  6. theorem OAI.RationalTetrahedron.referenceTetrahedron_isClosed line 41
  7. theorem OAI.RationalTetrahedron.referenceTetrahedron_isCompact line 58
  8. theorem OAI.RationalTetrahedron.space_integral_triple line 82
  9. theorem OAI.RationalTetrahedron.space_integrable_triple line 87
  10. theorem OAI.RationalTetrahedron.volume_by_slices line 94
  11. theorem OAI.RationalTetrahedron.tetrahedron_slice line 121
  12. theorem OAI.RationalTetrahedron.scaled_height_mem_iff line 138
  13. theorem OAI.RationalTetrahedron.volume_slice_integral line 155
  14. theorem OAI.RationalTetrahedron.referenceTetrahedron_volume line 177
  15. theorem OAI.SlopeRational.referenceTetrahedron_volume line 207