ReducedWalks.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SimpleGraph.Walk.Reduced line 16
Source documentation
A walk has no immediate backtracking when it has no closed subwalk of length two. This formulation is hereditary under taking subwalks.
```
def Walk.Reduced {u v : V} (p : G.Walk u v) : Prop :=
…
```
lemma OAI.SimpleGraph.Walk.Reduced.of_isSubwalk line 19
lemma OAI.SimpleGraph.Walk.Reduced.copy line 24
theorem OAI.SimpleGraph.Walk.Reduced.exists_cycle line 31
Source documentation
A nonempty closed walk with no immediate backtracking contains a cycle no longer than itself. This is the girth fact used for facial boundaries.
```
theorem Walk.Reduced.exists_cycle {u : V} {p : G.Walk u u}
    (hp : _root_.OAI.SimpleGraph.Walk.Reduced p) (hne : ¬ p.Nil) :
    ∃ (v : V) (q : G.Walk v v), q.IsCycle ∧ q.length ≤ p.length := by
…
```
lemma OAI.SimpleGraph.Walk.Reduced.egirth_le line 60

lemma OAI.SimpleGraph.Walk.reduced_of_getVert line 66

Source documentation

The elementary vertex-index criterion for no immediate backtracking.

lemma Walk.reduced_of_getVert {u v : V} (p : G.Walk u v)
    (h : ∀ i, i + 2 ≤ p.length → p.getVert i ≠ p.getVert (i + 2)) : _root_.OAI.SimpleGraph.Walk.Reduced p := by
…