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

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The eight local pulse endpoints for one filled source rectangle.

  1. theorem OAI.ForcedComputation.PlanarRouting.mem_translationTube_left line 14
  2. theorem OAI.ForcedComputation.PlanarRouting.mem_translationTube_right line 23
  3. theorem OAI.ForcedComputation.PlanarRouting.recenter_mem line 33
  4. theorem OAI.ForcedComputation.PlanarRouting.recenter_twice line 39
  5. theorem OAI.ForcedComputation.PlanarRouting.recenter_self line 49
  6. def OAI.ForcedComputation.Recorder.Planar.horizontalPoint line 62
  7. def OAI.ForcedComputation.Recorder.Planar.branchAnchors line 65
  8. theorem OAI.ForcedComputation.Recorder.Planar.branchAnchors_first line 78
  9. theorem OAI.ForcedComputation.Recorder.Planar.branchAnchors_last line 81
  10. theorem OAI.ForcedComputation.Recorder.Planar.branchAnchors_endpoint line 85
  11. theorem OAI.ForcedComputation.Recorder.Planar.branchAnchors_mem_rectangle line 126
  12. theorem OAI.ForcedComputation.Recorder.Planar.branch_curve_mem_rectangle line 176