OAI/Combinatorics/PolynomialVacuum/Cylinder/FinitePartition.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PolynomialVacuumCylinder.BoundedPolygon line 9
2. instance OAI.PolynomialVacuumCylinder.boundedPolygon_finite line 10
3. instance OAI.PolynomialVacuumCylinder.(instance at line 16) line 16
4. def OAI.PolynomialVacuumCylinder.boundedPolygons line 17
5. theorem OAI.PolynomialVacuumCylinder.mem_boundedPolygons line 19
6. abbrev OAI.PolynomialVacuumCylinder.BoundedSystem line 26
7. instance OAI.PolynomialVacuumCylinder.boundedSystem_finite line 28
8. instance OAI.PolynomialVacuumCylinder.(instance at line 35) line 35
9. abbrev OAI.PolynomialVacuumCylinder.BoundedOrientation line 37
10. abbrev OAI.PolynomialVacuumCylinder.BoundedFlow line 39
11. def OAI.PolynomialVacuumCylinder.boundedOrientationSigma line 41
12. instance OAI.PolynomialVacuumCylinder.(instance at line 48) line 48
13. def OAI.PolynomialVacuumCylinder.boundedOrientationEquiv line 51
14. instance OAI.PolynomialVacuumCylinder.(instance at line 58) line 58
15. theorem OAI.PolynomialVacuumCylinder.finite_current_partition line 63