PathColumnCrossing.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.CrossingBridge.path_column_subcrossing line 10

Source documentation

Last-left/first-right subcrossing from an actual finite path. The middle path stays between the two columns; both outside pieces are retained.

theorem path_column_subcrossing (p : Vertex) (ds : List Step) (A B : ℤ)
    (hp : p.1 ≤ A) (hAB : A ≤ B) (hend : B ≤ (p+displacement ds).1) :
    ∃ pre mid post : List Step, ds=pre++mid++post ∧
      (p+displacement pre).1=A ∧
      (p+displacement pre+displacement mid).1=B ∧
      PathIn (p+displacement pre) mid {z | A ≤ z.1 ∧ z.1 ≤ B} := by
…

Mentions: OAI.GammaFPP.CrossingBridge.PathIn

lemma OAI.GammaFPP.CrossingBridge.pathIn_middle line 46
Source documentation
Any middle part of a path inherits the original vertex localization.
```
lemma pathIn_middle (p : Vertex) (pre mid post : List Step) (S : Set Vertex)
    (h : PathIn p (pre++mid++post) S) : PathIn (p+displacement pre) mid S :=
…
```
Mentions: OAI.GammaFPP.CrossingBridge.PathIn