OAI/Combinatorics/HoneycombCorridor/Cells.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PolynomialVacuumBridge.Corridor.faceEdgesline 10 - def
OAI.PolynomialVacuumBridge.Corridor.faceVerticesline 15 - def
OAI.PolynomialVacuumBridge.Corridor.cellEdgesline 19 - def
OAI.PolynomialVacuumBridge.Corridor.cellVerticesline 21 - theorem
OAI.PolynomialVacuumBridge.Corridor.mem_faceEdgesline 23 - theorem
OAI.PolynomialVacuumBridge.Corridor.mem_faceVerticesline 30 - theorem
OAI.PolynomialVacuumBridge.Corridor.mem_cellEdgesline 36 - theorem
OAI.PolynomialVacuumBridge.Corridor.mem_cellVerticesline 47 - theorem
OAI.PolynomialVacuumBridge.Corridor.edge_mem_vertexline 56 - theorem
OAI.PolynomialVacuumBridge.Corridor.edgeOf_reverseline 77 - theorem
OAI.PolynomialVacuumBridge.Corridor.edge_mem_neighborline 81