OAI/Combinatorics/HoneycombCorridor/PolygonSize.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.graphDegree line 10
  2. theorem OAI.PolynomialVacuumBridge.Corridor.graphDegree_incidence line 13
  3. theorem OAI.PolynomialVacuumBridge.Corridor.graphDegree_sum line 37
  4. theorem OAI.PolynomialVacuumBridge.Corridor.Polygon.degree_two line 54
  5. theorem OAI.PolynomialVacuumBridge.Corridor.Polygon.length_eq_card_vertices line 67
  6. theorem OAI.PolynomialVacuumBridge.Corridor.Polygon.Traverses.length line 77
  7. theorem OAI.PolynomialVacuumBridge.Corridor.Polygon.length_pos line 81
  8. theorem OAI.PolynomialVacuumBridge.Corridor.sum_record_fibers line 88
  9. theorem OAI.PolynomialVacuumBridge.Corridor.excursions_fibers line 105
  10. theorem OAI.PolynomialVacuumBridge.Corridor.firstArrivals_fibers line 119
  11. theorem OAI.PolynomialVacuumBridge.Corridor.boundary_marked_eq_exits line 131
  12. theorem OAI.PolynomialVacuumBridge.Corridor.visitSum_eq_firstArrivals line 152
  13. theorem OAI.PolynomialVacuumBridge.Corridor.rayExits_eq_visitSum line 164