OAI/Combinatorics/PolynomialVacuum/Cylinder/NetworkDecomposition.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PolynomialVacuumCylinder.ClosedNetwork.outEdgeline 10 - theorem
OAI.PolynomialVacuumCylinder.ClosedNetwork.mem_word_edgesline 12 - theorem
OAI.PolynomialVacuumCylinder.ClosedNetwork.mem_polygon_edgesline 28 - theorem
OAI.PolynomialVacuumCylinder.ClosedNetwork.polygon_eq_of_sameCycleline 42 - theorem
OAI.PolynomialVacuumCylinder.ClosedNetwork.polygon_eq_of_overlapline 51 - def
OAI.PolynomialVacuumCylinder.ClosedNetwork.polygonsline 60 - theorem
OAI.PolynomialVacuumCylinder.ClosedNetwork.polygons_disjointline 62 - theorem
OAI.PolynomialVacuumCylinder.ClosedNetwork.polygons_verticesline 70 - theorem
OAI.PolynomialVacuumCylinder.ClosedNetwork.polygons_edgesline 82 - theorem
OAI.PolynomialVacuumCylinder.ClosedNetwork.polygons_total_lengthline 96