OAI/Combinatorics/HoneycombCorridor/Convexity.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.boxIndex line 10
  2. def OAI.PolynomialVacuumBridge.Corridor.BoxMem line 14
  3. theorem OAI.PolynomialVacuumBridge.Corridor.tilingCoordinate_index line 17
  4. theorem OAI.PolynomialVacuumBridge.Corridor.integer_bounds_fraction line 49
  5. theorem OAI.PolynomialVacuumBridge.Corridor.admissiblyConvex_box line 67
  6. def OAI.PolynomialVacuumBridge.Corridor.starFaces line 78
  7. theorem OAI.PolynomialVacuumBridge.Corridor.mem_starFaces line 81
  8. theorem OAI.PolynomialVacuumBridge.Corridor.incident_mem_starFaces line 87
  9. theorem OAI.PolynomialVacuumBridge.Corridor.box_opposite_face line 94
  10. theorem OAI.PolynomialVacuumBridge.Corridor.outside_opposite_face line 104
  11. theorem OAI.PolynomialVacuumBridge.Corridor.box_two_faces_up0 line 113
  12. theorem OAI.PolynomialVacuumBridge.Corridor.box_two_faces_up1 line 126
  13. theorem OAI.PolynomialVacuumBridge.Corridor.box_two_faces_up2 line 139
  14. theorem OAI.PolynomialVacuumBridge.Corridor.box_two_faces_down0 line 152
  15. theorem OAI.PolynomialVacuumBridge.Corridor.box_two_faces_down1 line 165
  16. theorem OAI.PolynomialVacuumBridge.Corridor.box_two_faces_down2 line 178
  17. theorem OAI.PolynomialVacuumBridge.Corridor.box_two_faces line 191