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

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

In an unused global slot a branch can only be at its source, at one of its two parked endpoints, or at its final target.

  1. theorem OAI.ForcedComputation.Recorder.Planar.branchIndices_adjacent line 17
  2. theorem OAI.ForcedComputation.Recorder.Planar.branch_unused_windows line 28
  3. theorem OAI.ForcedComputation.Recorder.Planar.sparseAnchor_source line 43
  4. theorem OAI.ForcedComputation.Recorder.Planar.sparseAnchor_parkedSource line 50
  5. theorem OAI.ForcedComputation.Recorder.Planar.sparseAnchor_parkedTarget line 60
  6. theorem OAI.ForcedComputation.Recorder.Planar.sparseAnchor_target line 71
  7. theorem OAI.ForcedComputation.Recorder.Planar.parkedSource_mem line 79
  8. theorem OAI.ForcedComputation.Recorder.Planar.parkedTarget_mem line 88
  9. theorem OAI.ForcedComputation.Recorder.Planar.ownPhase_surjective line 99
  10. theorem OAI.ForcedComputation.Recorder.Planar.unused_owner_ne line 113