OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/PlanarTubes.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Clearance for the actual filled extraction and insertion tubes.

  1. theorem OAI.ForcedComputation.PlanarRouting.box_ext line 12
  2. theorem OAI.ForcedComputation.PlanarRouting.centerQ_sub_halfWidthQ line 19
  3. theorem OAI.ForcedComputation.PlanarRouting.centerQ_add_halfWidthQ line 24
  4. def OAI.ForcedComputation.PlanarRouting.horizontalCenter line 29
  5. theorem OAI.ForcedComputation.PlanarRouting.horizontalTube_eq_rightSweep line 33
  6. def OAI.ForcedComputation.PlanarRouting.parkingColumn line 49
  7. theorem OAI.ForcedComputation.PlanarRouting.parkingColumn_gap line 52
  8. theorem OAI.ForcedComputation.PlanarRouting.parkingColumn_left line 58
  9. theorem OAI.ForcedComputation.PlanarRouting.low_horizontal_gap_column line 67
  10. theorem OAI.ForcedComputation.PlanarRouting.parkingBox_subset_column line 74
  11. theorem OAI.ForcedComputation.PlanarRouting.verticalTube_subset_column line 84