OAI/Combinatorics/HoneycombCorridor/Polygons.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.SimplePolygonTurning line 11
  2. theorem OAI.PolynomialVacuumBridge.Corridor.simple_polygon_signed_turn line 15
  3. theorem OAI.PolynomialVacuumBridge.Corridor.simple_polygon_turning line 39
  4. def OAI.PolynomialVacuumBridge.Corridor.IsPolygon line 48
  5. abbrev OAI.PolynomialVacuumBridge.Corridor.Polygon line 51
  6. def OAI.PolynomialVacuumBridge.Corridor.Polygon.germ line 54
  7. def OAI.PolynomialVacuumBridge.Corridor.Polygon.turns line 55
  8. theorem OAI.PolynomialVacuumBridge.Corridor.Polygon.traversal line 57
  9. theorem OAI.PolynomialVacuumBridge.Corridor.Polygon.has_indicator line 62
  10. def OAI.PolynomialVacuumBridge.Corridor.Polygon.potential line 67
  11. def OAI.PolynomialVacuumBridge.Corridor.Polygon.orientation line 68
  12. theorem OAI.PolynomialVacuumBridge.Corridor.Polygon.potential_spec line 70
  13. def OAI.PolynomialVacuumBridge.Corridor.Polygon.interiorFaces line 76
  14. def OAI.PolynomialVacuumBridge.Corridor.Polygon.vertices line 78
  15. def OAI.PolynomialVacuumBridge.Corridor.Polygon.interior line 80
  16. def OAI.PolynomialVacuumBridge.Corridor.Polygon.length line 83
  17. def OAI.PolynomialVacuumBridge.Corridor.Polygon.ccwTurn line 85
  18. def OAI.PolynomialVacuumBridge.Corridor.inducedEdges line 89
  19. def OAI.PolynomialVacuumBridge.Corridor.polygons line 93
  20. def OAI.PolynomialVacuumBridge.Corridor.Filled line 97
  21. def OAI.PolynomialVacuumBridge.Corridor.visitMass line 99
  22. def OAI.PolynomialVacuumBridge.Corridor.excursionMass line 101
  23. def OAI.PolynomialVacuumBridge.Corridor.polygonSystems line 105
  24. def OAI.PolynomialVacuumBridge.Corridor.faceNestingMass line 112
  25. def OAI.PolynomialVacuumBridge.Corridor.tilingCoordinate line 115
  26. def OAI.PolynomialVacuumBridge.Corridor.AdmissiblyConvex line 120
  27. def OAI.PolynomialVacuumBridge.Corridor.FiniteVisitRecursion line 125
  28. def OAI.PolynomialVacuumBridge.Corridor.FiniteVisitsTheorem line 133