OAI/Combinatorics/HoneycombCorridor/Curvature.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.turnUnit line 10
  2. def OAI.PolynomialVacuumBridge.Corridor.turnUnits line 12
  3. def OAI.PolynomialVacuumBridge.Corridor.faceCount line 14
  4. def OAI.PolynomialVacuumBridge.Corridor.edgeCount line 17
  5. def OAI.PolynomialVacuumBridge.Corridor.cellCurvature line 20
  6. theorem OAI.PolynomialVacuumBridge.Corridor.rightFace_prev line 23
  7. theorem OAI.PolynomialVacuumBridge.Corridor.leftFace_injective line 27
  8. theorem OAI.PolynomialVacuumBridge.Corridor.faceCount_incidence line 31
  9. theorem OAI.PolynomialVacuumBridge.Corridor.edgeOf_slot line 56
  10. theorem OAI.PolynomialVacuumBridge.Corridor.edgeOf_canonical line 60
  11. theorem OAI.PolynomialVacuumBridge.Corridor.edgeOf_downEnd line 64
  12. theorem OAI.PolynomialVacuumBridge.Corridor.edgeOf_eq_iff line 68
  13. theorem OAI.PolynomialVacuumBridge.Corridor.upEnd_ne_downEnd line 83
  14. theorem OAI.PolynomialVacuumBridge.Corridor.edgeCount_incidence line 87
  15. theorem OAI.PolynomialVacuumBridge.Corridor.faceVertices_card line 111
  16. theorem OAI.PolynomialVacuumBridge.Corridor.sum_faceCount line 115
  17. theorem OAI.PolynomialVacuumBridge.Corridor.sum_edgeCount line 133
  18. theorem OAI.PolynomialVacuumBridge.Corridor.sum_cellCurvature line 150
  19. theorem OAI.PolynomialVacuumBridge.Corridor.numeric_contour_curvature line 158
  20. theorem OAI.PolynomialVacuumBridge.Corridor.contour_cellCurvature line 177
  21. theorem OAI.PolynomialVacuumBridge.Corridor.nonboundary_cellCurvature line 193
  22. theorem OAI.PolynomialVacuumBridge.Corridor.contour_curvature_sum line 212