OAI/Geometry/CylinderCovering/Rational/TetrahedronGeometry.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RationalSimilarity.sqrtTwo_pos line 10
  2. theorem OAI.RationalSimilarity.sqrtTwo_sq line 11
  3. theorem OAI.RationalSimilarity.h_eq_sqrt_half line 13
  4. theorem OAI.RationalSimilarity.uncenteredTetrahedron_eq_dilation line 18
  5. def OAI.RationalSimilarity.dilation line 53
  6. theorem OAI.RationalSimilarity.dilation_apply line 56
  7. theorem OAI.RationalSimilarity.dilation_injective line 59
  8. theorem OAI.RationalSimilarity.vertices_eq_dilation line 62
  9. theorem OAI.RationalSimilarity.uncenteredVertices_affineIndependent line 70
  10. theorem OAI.RationalSimilarity.uncenteredVertices_edge line 74
  11. theorem OAI.RationalSimilarity.uncenteredTetrahedron_eq_convexHull line 82
  12. theorem OAI.RationalSimilarity.uncenteredTetrahedron_regular line 90
  13. theorem OAI.RationalSimilarity.uncenteredTetrahedron_geometry line 96