OAI/Geometry/TriangularCovering/Tetrahedron.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TriangularCovering.faceNormal line 11
  2. def OAI.TriangularCovering.faceBound line 12
  3. def OAI.TriangularCovering.faceVertices line 13
  4. def OAI.TriangularCovering.face line 18
  5. lemma OAI.TriangularCovering.point_coord line 20
  6. lemma OAI.TriangularCovering.K_halfspaces line 25
  7. lemma OAI.TriangularCovering.K_convex line 43
  8. lemma OAI.TriangularCovering.face_vertices_mem line 50
  9. lemma OAI.TriangularCovering.face_convex line 60
  10. lemma OAI.TriangularCovering.face_eq_triangle line 63
  11. lemma OAI.TriangularCovering.face_cross line 108
  12. lemma OAI.TriangularCovering.face_projection_measure line 114
  13. def OAI.TriangularCovering.tetraVertices line 129

    Source documentation

    The four vertices of the regular tetrahedron.

    def tetraVertices : Fin 4 → Space :=
…

    Mentions: OAI.TriangularCovering.Space

  14. lemma OAI.TriangularCovering.tetraVertices_mem line 132
  15. lemma OAI.TriangularCovering.K_eq_convexHull line 139
  16. lemma OAI.TriangularCovering.K_compact line 154
  17. lemma OAI.TriangularCovering.K_interior_nonempty line 158
  18. lemma OAI.TriangularCovering.tetra_edge_length line 173
  19. lemma OAI.TriangularCovering.tetra_affineIndependent line 183
  20. def OAI.TriangularCovering.tetraSimplex line 195
  21. lemma OAI.TriangularCovering.tetraSimplex_equilateral line 197
  22. theorem OAI.TriangularCovering.tetrahedron_geometry line 201

    Source documentation

    The tetrahedron is compact, convex, and full dimensional, with six edges of length 2.

    theorem tetrahedron_geometry :
    K = convexHull ℝ (range tetraVertices) ∧ IsCompact K ∧ Convex ℝ K ∧
    (interior K).Nonempty ∧ ∀ i j : Fin 4, i ≠ j → dist (tetraVertices i) (tetraVertices j) = 2 :=
…

    Mentions: OAI.TriangularCovering.K, OAI.TriangularCovering.tetraVertices