OAI/Combinatorics/HoneycombCorridor/IntegerPotential.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PolynomialVacuumBridge.Corridor.FaceIndex line 9
  2. def OAI.PolynomialVacuumBridge.Corridor.facePrefix line 11
  3. theorem OAI.PolynomialVacuumBridge.Corridor.facePrefix_difference line 14
  4. def OAI.PolynomialVacuumBridge.Corridor.InFaceBox line 38
  5. def OAI.PolynomialVacuumBridge.Corridor.faceRadius line 41
  6. theorem OAI.PolynomialVacuumBridge.Corridor.mem_support_in_box line 44
  7. theorem OAI.PolynomialVacuumBridge.Corridor.facePrefix_left_zero line 53
  8. theorem OAI.PolynomialVacuumBridge.Corridor.facePrefix_row_zero line 62
  9. theorem OAI.PolynomialVacuumBridge.Corridor.int_function_constant line 72
  10. structure OAI.PolynomialVacuumBridge.Corridor.FiniteHoneycombFlow line 83
  11. def OAI.PolynomialVacuumBridge.Corridor.flowPotential line 90
  12. theorem OAI.PolynomialVacuumBridge.Corridor.flow_difference line 93
  13. theorem OAI.PolynomialVacuumBridge.Corridor.flowPotential_vertical line 99
  14. theorem OAI.PolynomialVacuumBridge.Corridor.flowPotential_right_zero line 127
  15. theorem OAI.PolynomialVacuumBridge.Corridor.flowPotential_finite_support line 144
  16. def OAI.PolynomialVacuumBridge.Corridor.finiteFlowPotential line 166
  17. theorem OAI.PolynomialVacuumBridge.Corridor.finite_flow_is_face_boundary line 170