OAI/Combinatorics/HoneycombCorridor/CollisionCancellation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolynomialVacuumBridge.Corridor.polygonOfClosed line 11
2. theorem OAI.PolynomialVacuumBridge.Corridor.polygonOfClosed_vertices line 15
3. theorem OAI.PolynomialVacuumBridge.Corridor.mem_traced_split line 20
4. theorem OAI.PolynomialVacuumBridge.Corridor.reverseAt_append line 31
5. theorem OAI.PolynomialVacuumBridge.Corridor.split_back_not_mem line 41
6. theorem OAI.PolynomialVacuumBridge.Corridor.root_collision_cancels line 53
7. theorem OAI.PolynomialVacuumBridge.Corridor.boundary_collision_pair line 87
8. theorem OAI.PolynomialVacuumBridge.Corridor.collision_subsum_zero line 128
9. theorem OAI.PolynomialVacuumBridge.Corridor.boundary_collision_cancellation line 145