module module

`IndisputableMonolith.Geometry.FreudenthalTwoCubeStrip`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.FreudenthalCubeTriangulation module_import

declarations in this module (16)

abbrev V L27
abbrev E L28
abbrev T L29
def edgeVerts L32
def globalSqEdge L68
def tetVerts L105
def localEdgeOf L156
def edgeInTet L230
def twoCubeStrip L239
theorem edgeInTet_iff_localEdgeOf L248
theorem local_sqEdge_eq_global L252
theorem edgeInTet_vertices L261
theorem localEdge_complete L273
def twoCubeStrip_incidenceConsistent L277
def twoCubeStrip_edgeSlotPartition L293
def twoCubeStrip_edgeSlotBookkeeping L300