OAI/Combinatorics/PolynomialVacuum/Bridge/ConfinedFiniteness.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PolynomialVacuumBridge.Corridor.windowline 7 - theorem
OAI.PolynomialVacuumBridge.Corridor.window_finiteline 10 - abbrev
OAI.PolynomialVacuumBridge.Corridor.CorridorVertexline 49 - def
OAI.PolynomialVacuumBridge.Corridor.corridorListline 52 - theorem
OAI.PolynomialVacuumBridge.Corridor.corridorList_valline 58 - theorem
OAI.PolynomialVacuumBridge.Corridor.corridorList_nodupline 63 - theorem
OAI.PolynomialVacuumBridge.Corridor.confined_paths_finiteline 69 - theorem
OAI.PolynomialVacuumBridge.Corridor.confined_finite_sumsline 87