module
module
IndisputableMonolith.Geometry.Triangulation3DConsistency
show as:
view Lean formalization →
used by (1)
depends on (2)
declarations in this module (11)
-
structure
IncidenceConsistent -
theorem
is -
structure
IncidenceGeometry -
def
globalEdgeLength -
theorem
localSqEdge_eq_globalSqEdge -
theorem
localEdgeLength_eq_globalEdgeLength -
def
triangulationSchlaefliData_of_incidence -
theorem
global_schlaefli_from_incidence -
theorem
nonempty_triangulationSchlaefliData_of_incidence -
def
triangulationSchlaefliData_of_geometry -
theorem
global_schlaefli_from_geometry