OAI/Combinatorics/HoneycombCorridor/CollisionStems.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.stemEnd line 11
  2. def OAI.PolynomialVacuumBridge.Corridor.IsPolygonStem line 13
  3. def OAI.PolynomialVacuumBridge.Corridor.polygonStems line 17
  4. theorem OAI.PolynomialVacuumBridge.Corridor.mem_polygonStems line 22
  5. theorem OAI.PolynomialVacuumBridge.Corridor.IsPolygonStem.trace_disjoint line 28
  6. theorem OAI.PolynomialVacuumBridge.Corridor.IsPolygonStem.back_outside line 35
  7. theorem OAI.PolynomialVacuumBridge.Corridor.Polygon.neighbor_mem_of_edge line 42
  8. theorem OAI.PolynomialVacuumBridge.Corridor.thirdSlot_unique line 47
  9. theorem OAI.PolynomialVacuumBridge.Corridor.stemGerm_eq_of_back_outside line 53
  10. def OAI.PolynomialVacuumBridge.Corridor.attachWord line 67
  11. theorem OAI.PolynomialVacuumBridge.Corridor.attachWord_injective_on_words line 72
  12. theorem OAI.PolynomialVacuumBridge.Corridor.attached_trace line 84
  13. theorem OAI.PolynomialVacuumBridge.Corridor.first_cut_unique line 99
  14. def OAI.PolynomialVacuumBridge.Corridor.spliceRecord line 119
  15. def OAI.PolynomialVacuumBridge.Corridor.rayCollisions line 122
  16. theorem OAI.PolynomialVacuumBridge.Corridor.mem_rayCollisions line 126
  17. theorem OAI.PolynomialVacuumBridge.Corridor.spliceRecord_mem line 132