OAI/Combinatorics/HoneycombCorridor/BoundaryArcs.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumBridge.Corridor.turnUnits_append line 11
  2. theorem OAI.PolynomialVacuumBridge.Corridor.reverse_stem_false line 15
  3. theorem OAI.PolynomialVacuumBridge.Corridor.reverse_advance_true line 18
  4. theorem OAI.PolynomialVacuumBridge.Corridor.chord_close_trace line 22
  5. theorem OAI.PolynomialVacuumBridge.Corridor.chord_close_terminal line 34
  6. theorem OAI.PolynomialVacuumBridge.Corridor.chord_close_turn line 44
  7. theorem OAI.PolynomialVacuumBridge.Corridor.cycle_chord_turn_bound line 94
  8. theorem OAI.PolynomialVacuumBridge.Corridor.faceBoundaryWord_append line 133
  9. theorem OAI.PolynomialVacuumBridge.Corridor.boundary_stem_port line 142
  10. theorem OAI.PolynomialVacuumBridge.Corridor.boundary_inward_port line 146
  11. theorem OAI.PolynomialVacuumBridge.Corridor.convex_distinct_outer_vertices line 150
  12. theorem OAI.PolynomialVacuumBridge.Corridor.boundary_chord_turn_bound line 166
  13. theorem OAI.PolynomialVacuumBridge.Corridor.convex_excursion_turn_bound line 213