OAI/Combinatorics/PolynomialVacuum/Cylinder/OpenEquiv.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolynomialVacuumCylinder.arcs_unique_of_eq line 10
2. theorem OAI.PolynomialVacuumCylinder.ArcClosedData.current_injective line 19
3. theorem OAI.PolynomialVacuumCylinder.ArcClosedData.exists_of_flow line 39
4. def OAI.PolynomialVacuumCylinder.openFlowEquiv line 57
5. theorem OAI.PolynomialVacuumCylinder.band_partition_arcs line 67