theorem WList.WellFormed.rotate_toGraph {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.WellFormed) (h_closed : w.IsClosed) (n : ℕ) : (w.rotate n).toGraph = w.toGraph

theorem Graph.IsWalk.rotate {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} (hw : G.IsWalk w) (hc : w.IsClosed) (n : ℕ) : G.IsWalk (w.rotate n)

theorem Graph.IsWalk.intRotate {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} (hw : G.IsWalk w) (hc : w.IsClosed) (n : ℤ) : G.IsWalk (w.intRotate n)

@[simp]

theorem Graph.IsClosed.isWalk_rotate_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} (hc : w.IsClosed) {n : ℕ} : G.IsWalk (w.rotate n) ↔ G.IsWalk w

structure Graph.IsTour {α : Type u_1} {β : Type u_2} (G : Graph α β) (C : WList α β) extends G.IsTrail C : Prop

G.IsTour C means that C is a nonempty closed walk with no repeated edges (but possibly repeated vertices).

• isWalk : G.IsWalk C
• edge_nodup : C.edge.Nodup
• nonempty : C.Nonempty
• isClosed : C.IsClosed

  The start and end vertex are the same

theorem Graph.isTour_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (C : WList α β) : G.IsTour C ↔ G.IsTrail C ∧ C.Nonempty ∧ C.IsClosed

structure Graph.IsCyclicWalk {α : Type u_1} {β : Type u_2} (G : Graph α β) (C : WList α β) extends G.IsTour C : Prop

G.IsCyclicWalk C means that C is a nonempty closed walk with no repeated vertices or edges.

• isWalk : G.IsWalk C
• edge_nodup : C.edge.Nodup
• nonempty : C.Nonempty
• isClosed : C.IsClosed
• nodup : C.tail.vertex.Nodup

  There are no repeated vertices except for the first and last.

theorem Graph.isCyclicWalk_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (C : WList α β) : G.IsCyclicWalk C ↔ G.IsTour C ∧ C.tail.vertex.Nodup

theorem Graph.IsWalk.isCyclicWalk_of_closed_nodup {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsWalk C) (hlen : 2 < C.length) (h_closed : C.IsClosed) (nodup : C.tail.vertex.Nodup) : G.IsCyclicWalk C

If C has at least three edges, then the assumption that C has distinct edges follows from its distinct vertices, so is not needed.

theorem Graph.IsTour.isCyclicWalk_of_dropLast_nodup {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (h : G.IsTour C) (hC : C.dropLast.vertex.Nodup) : G.IsCyclicWalk C

theorem Graph.IsTour.isTrail {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsTour C) : G.IsTrail C

@[simp]

theorem Graph.not_isTour_nil {α : Type u_1} {β : Type u_2} {G : Graph α β} (x : α) : ¬G.IsTour (WList.nil x)

theorem Graph.IsTour.rotate {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsTour C) (n : ℕ) : G.IsTour (C.rotate n)

theorem Graph.IsTour.intRotate {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsTour C) (n : ℤ) : G.IsTour (C.intRotate n)

theorem Graph.IsTour.reverse {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsTour C) : G.IsTour C.reverse

theorem Graph.IsCyclicWalk.reverse {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) : G.IsCyclicWalk C.reverse

theorem Graph.IsTour.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {C : WList α β} (hC : H.IsTour C) (hle : H ≤ G) : G.IsTour C

theorem Graph.IsTour.of_le_of_subset {α : Type u_1} {β : Type u_2} {G H : Graph α β} {w : WList α β} (h : G.IsTour w) (hle : H ≤ G) (hE : w.edgeSet ⊆ H.edgeSet) : H.IsTour w

theorem Graph.IsTour.isTour_toGraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsTour C) : C.toGraph.IsTour C

theorem Graph.IsTour.of_forall_isLink {α : Type u_1} {β : Type u_2} {G H : Graph α β} {C : WList α β} (h : G.IsTour C) (he : ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → H.IsLink e x y) : H.IsTour C

@[simp]

theorem Graph.restrict_isTour_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (F : Set β) (C : WList α β) : (G.restrict F).IsTour C ↔ G.IsTour C ∧ C.edgeSet ⊆ F

@[simp]

theorem Graph.deleteEdges_isTour_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (F : Set β) (C : WList α β) : (G.deleteEdges F).IsTour C ↔ G.IsTour C ∧ Disjoint C.edgeSet F

@[simp]

theorem Graph.induce_isTour_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (X : Set α) (C : WList α β) : G[X].IsTour C ↔ G.IsTour C ∧ C.vertexSet ⊆ X

@[simp]

theorem Graph.deleteVerts_isTour_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (X : Set α) (C : WList α β) : (G.deleteVerts X).IsTour C ↔ G.IsTour C ∧ Disjoint C.vertexSet X

theorem Graph.IsTrail.dedup {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} [DecidableEq α] (hC : G.IsTrail C) : G.IsTrail C.dedup

Dedup preserves being a trail (walk with distinct edges).

theorem Graph.IsTour.dedup_tail_isCyclicWalk {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {w : WList α β} [DecidableEq α] (hC : G.IsTour (WList.cons x e w)) : G.IsCyclicWalk (WList.cons x e w.dedup)

Applying dedup to the tail of a tour gives a cycle.

theorem Graph.IsTrail.cycleBypass_isSimple {α : Type u_1} {β : Type u_2} {G : Graph α β} [DecidableEq α] {w : WList α β} (hw : G.IsTrail w) : G.IsPath w.cycleBypass ∨ G.IsCyclicWalk w.cycleBypass

theorem Graph.IsTrail.cycleBypass_eq_self_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} [DecidableEq α] {w : WList α β} (hw : G.IsTrail w) : w.cycleBypass = w ↔ G.IsPath w ∨ G.IsCyclicWalk w

WList.cycleBypass fixes exactly the paths and cyclic walks among trails.

theorem Graph.IsTour.exists_isCyclicWalk {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsTour C) : ∃ (C' : WList α β), G.IsCyclicWalk C' ∧ C'.IsSublist C

Every tour contains a cycle as a sublist.

theorem Graph.IsCyclicWalk.isTour {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) : G.IsTour C

theorem Graph.IsCyclicWalk.idxOf_get {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} [DecidableEq α] (hC : G.IsCyclicWalk C) {n : ℕ} (hn : n < C.length) : C.idxOf (C.get n) = n

theorem Graph.IsCyclicWalk.isTrail {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) : G.IsTrail C

theorem Graph.IsCyclicWalk.rotate {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) (n : ℕ) : G.IsCyclicWalk (C.rotate n)

@[simp]

theorem Graph.not_isCyclicWalk_nil {α : Type u_1} {β : Type u_2} {G : Graph α β} (x : α) : ¬G.IsCyclicWalk (WList.nil x)

theorem Graph.IsTour.edgeRemove {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {F : Set β} [DecidablePred fun (x : β) => x ∈ F] (hw : G.IsTour w) (hF : ∀ e ∈ w.edge, e ∈ F → ∃ (x : α), G.IsLoopAt e x) (hne : ∃ e ∈ w.edge, e ∉ F) : G.IsTour (WList.edgeRemove F w)

theorem Graph.IsCyclicWalk.intRotate {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) (n : ℤ) : G.IsCyclicWalk (C.intRotate n)

theorem Graph.IsCyclicWalk.rotate_one {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) : ∃ (e : β), C.rotate 1 = C.tail.concat e C.tail.first

theorem Graph.IsCyclicWalk.idxOf_rotate_one {α : Type u_1} {β : Type u_2} {a : α} {G : Graph α β} {C : WList α β} [DecidableEq α] (hC : G.IsCyclicWalk C) (h1 : C.first ≠ a) (ha : a ∈ C) : (C.rotate 1).idxOf a + 1 = C.idxOf a

theorem Graph.IsCyclicWalk.idxOf_rotate_first {α : Type u_1} {β : Type u_2} {a : α} {G : Graph α β} {C : WList α β} {n : ℕ} [DecidableEq α] : G.IsCyclicWalk C → ∀ (hlt : n < C.idxOf a), (C.rotate n).first ≠ a

theorem Graph.IsCyclicWalk.idxOf_rotate_n_le {α : Type u_1} {β : Type u_2} {a : α} {G : Graph α β} {C : WList α β} {n : ℕ} [DecidableEq α] : G.IsCyclicWalk C → ∀ (ha : a ∈ C) (hle : n ≤ C.idxOf a), (C.rotate n).idxOf a + n = C.idxOf a

theorem Graph.IsCyclicWalk.idxOf_rotate_one_first' {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} [DecidableEq α] (hC : G.IsCyclicWalk C) : (C.rotate 1).idxOf C.first + 1 = C.length

theorem Graph.IsCyclicWalk.idxOf_rotate_one_first {α : Type u_1} {β : Type u_2} {a : α} {G : Graph α β} {C : WList α β} [DecidableEq α] (hC : G.IsCyclicWalk C) (h1 : C.first = a) (ha : a ∈ C) : (C.rotate 1).idxOf a + 1 = C.length

theorem Graph.IsCyclicWalk.idxOf_rotate_untilfirst {α : Type u_1} {β : Type u_2} {a : α} {G : Graph α β} {C : WList α β} [DecidableEq α] (hC : G.IsCyclicWalk C) (ha : a ∈ C) : (C.rotate (C.idxOf a + 1)).idxOf a + 1 = C.length

theorem Graph.IsCyclicWalk.idxOf_rotate_idxOf {α : Type u_1} {β : Type u_2} {a : α} {G : Graph α β} {C : WList α β} [DecidableEq α] (hC : G.IsCyclicWalk C) (ha : a ∈ C) : (C.rotate (C.idxOf a)).idxOf a = 0

theorem Graph.IsCyclicWalk.idxOf_rotate_n {α : Type u_1} {β : Type u_2} {a : α} {G : Graph α β} {C : WList α β} {n : ℕ} [DecidableEq α] (hC : G.IsCyclicWalk C) (ha : a ∈ C) (hn : n < C.length) (hle : C.idxOf a < n) : (C.rotate n).idxOf a + n = C.length + C.idxOf a

theorem Graph.IsCyclicWalk.idxOf_adj {α : Type u_1} {β : Type u_2} {a b : α} {G : Graph α β} {C : WList α β} [DecidableEq α] (hC : G.IsCyclicWalk C) (ha : a ∈ C) (hb : b ∈ C) (he : C.idxOf b = C.idxOf a + 1) : G.Adj a b

theorem Graph.IsCyclicWalk.idxOf_adj_first {α : Type u_1} {β : Type u_2} {a b : α} {G : Graph α β} {C : WList α β} [DecidableEq α] (hC : G.IsCyclicWalk C) (hab : a ≠ b) (ha : C.idxOf a = 0) (hb : C.idxOf b = C.length - 1) : G.Adj a b

theorem Graph.IsCyclicWalk.idxOf_rotate {α : Type u_1} {β : Type u_2} {a : α} {G : Graph α β} {C : WList α β} {n : ℕ} [DecidableEq α] (hC : G.IsCyclicWalk C) (ha : a ∈ C) (hn : n < C.length) : ((C.rotate n).idxOf a + n) % C.length = C.idxOf a

theorem Graph.IsCyclicWalk.idxOf_adj_rotate {α : Type u_1} {β : Type u_2} {a b : α} {G : Graph α β} {C : WList α β} {n : ℕ} [DecidableEq α] (hC : G.IsCyclicWalk C) (ha : a ∈ C) (hb : b ∈ C) (hn : n < C.length) : C.idxOf b = C.idxOf a + 1 ∨ C.idxOf b = 0 ∧ C.idxOf a = C.length - 1 ↔ (C.rotate n).idxOf b = (C.rotate n).idxOf a + 1 ∨ (C.rotate n).idxOf b = 0 ∧ (C.rotate n).idxOf a = C.length - 1

theorem Graph.IsCyclicWalk.tail_isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) : G.IsPath C.tail

theorem Graph.IsCyclicWalk.dropLast_isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) : G.IsPath C.dropLast

theorem Graph.IsCyclicWalk.tail_dropLast_isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) : G.IsPath C.tail.dropLast

theorem Graph.IsCyclicWalk.eq_cons_concat {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) (hnt : C.Nontrivial) : ∃ (x : α) (e : β) (f : β) (P : WList α β), G.IsPath P ∧ x ∉ P ∧ e ∉ P.edge ∧ f ∉ P.edge ∧ C = WList.cons x e (P.concat f x)

theorem Graph.IsCyclicWalk.mem_tail_dropLast_of_ne_first {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) (hxC : x ∈ C) (hx : x ≠ C.first) : x ∈ C.tail.dropLast

theorem Graph.IsCyclicWalk.tail_dropLast_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) (hnt : C.Nontrivial) : C.tail.dropLast.vertexSet = C.vertexSet \ {C.first}

theorem Graph.IsCyclicWalk.eq_or_nil_of_isSublist_of_first_last_eq {α : Type u_1} {β : Type u_2} {G : Graph α β} {w C : WList α β} (hC : G.IsCyclicWalk C) (h : w ≤ C) (hfirst : w.first = C.first) (hlast : w.last = C.last) : w = C ∨ w = WList.nil w.first

theorem Graph.IsCyclicWalk.ne_iff_isPath_of_isSublist {α : Type u_1} {β : Type u_2} {G : Graph α β} {w C : WList α β} (hC : G.IsCyclicWalk C) (h : w ≤ C) : w ≠ C ↔ G.IsPath w

theorem Graph.IsCyclicWalk.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {C : WList α β} (hC : H.IsCyclicWalk C) (hle : H ≤ G) : G.IsCyclicWalk C

theorem Graph.IsCyclicWalk.isCycle_of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {w : WList α β} (h : G.IsCyclicWalk w) (hle : H ≤ G) (hE : w.edgeSet ⊆ H.edgeSet) : H.IsCyclicWalk w

theorem Graph.IsCyclicWalk.eq_loop_of_isLink_self {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {C : WList α β} (h : G.IsCyclicWalk C) (hC : C.IsLink e x x) : C = WList.cons x e (WList.nil x)

theorem Graph.IsCyclicWalk.isCyclicWalk_toGraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) : C.toGraph.IsCyclicWalk C

theorem Graph.IsCyclicWalk.ne_of_isLink {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) (hnt : C.Nontrivial) (hinc : C.IsLink e x y) : x ≠ y

theorem Graph.IsCyclicWalk.length_eq_one_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (h : G.IsCyclicWalk C) : C.length = 1 ↔ ∃ (x : α) (e : β), C = WList.cons x e (WList.nil x)

theorem Graph.IsCyclicWalk.length_eq_two_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (h : G.IsCyclicWalk C) : C.length = 2 ↔ ∃ (x : α) (y : α) (e : β) (f : β), x ≠ y ∧ e ≠ f ∧ C = WList.cons x e (WList.cons y f (WList.nil x))

theorem Graph.IsCyclicWalk.encard_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (h : G.IsCyclicWalk C) : C.vertexSet.encard = ↑C.length

theorem Graph.IsCyclicWalk.ncard_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (h : G.IsCyclicWalk C) : C.vertexSet.ncard = C.length

theorem Graph.IsCyclicWalk.loop_or_noloop {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (h : G.IsCyclicWalk C) : (∃ (x : α) (e : β), C = WList.cons x e (WList.nil x)) ∨ C.NoLoop

theorem Graph.IsCyclicWalk.noloop_of_nontrivial {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (h : G.IsCyclicWalk C) (hnt : C.Nontrivial) : C.NoLoop

@[simp]

theorem Graph.rotate_toGraph {α : Type u_1} {β : Type u_2} {C : WList α β} {n : ℕ} (hC : C.IsClosed) (hCwf : C.WellFormed) : (C.rotate n).toGraph = C.toGraph

@[simp]

theorem Graph.restrict_isCyclicWalk_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (F : Set β) (C : WList α β) : (G.restrict F).IsCyclicWalk C ↔ G.IsCyclicWalk C ∧ C.edgeSet ⊆ F

@[simp]

theorem Graph.deleteEdges_isCyclicWalk_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (F : Set β) (C : WList α β) : (G.deleteEdges F).IsCyclicWalk C ↔ G.IsCyclicWalk C ∧ Disjoint C.edgeSet F

@[simp]

theorem Graph.induce_isCyclicWalk_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (X : Set α) (C : WList α β) : G[X].IsCyclicWalk C ↔ G.IsCyclicWalk C ∧ C.vertexSet ⊆ X

@[simp]

theorem Graph.deleteVerts_isCyclicWalk_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (X : Set α) (C : WList α β) : (G.deleteVerts X).IsCyclicWalk C ↔ G.IsCyclicWalk C ∧ Disjoint C.vertexSet X

theorem Graph.IsCyclicWalk.of_forall_isLink {α : Type u_1} {β : Type u_2} {G H : Graph α β} {C : WList α β} (h : G.IsCyclicWalk C) (he : ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → H.IsLink e x y) : H.IsCyclicWalk C

theorem Graph.IsCyclicWalk.exists_isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) (hnt : C.Nontrivial) : ∃ (P : WList α β) (u : α) (e : β) (f : β), G.IsPath P ∧ u ∉ P ∧ e ∉ P.edge ∧ f ∉ P.edge ∧ e ≠ f ∧ C = WList.cons u e (P.concat f u)

theorem Graph.IsCyclicWalk.exists_isPath' {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) (hnt : C.Nontrivial) : ∃ (P : WList α β) (u : α) (e : β) (f : β), G.IsPath (WList.cons u e P) ∧ G.IsPath (P.concat f u) ∧ e ≠ f ∧ C = WList.cons u e (P.concat f u)

An alternative version of IsCyclicWalk.exists_isPath where the tail and the head of the cycle are explictly given as paths.

theorem Graph.IsCyclicWalk.exists_isPath_vertex {α : Type u_1} {β : Type u_2} {u : α} {G : Graph α β} {C : WList α β} [DecidableEq α] (hC : G.IsCyclicWalk C) (hnt : C.Nontrivial) (hu : u ∈ C) : ∃ (P : WList α β) (e : β) (f : β), G.IsPath P ∧ u ∉ P ∧ e ∉ P.edge ∧ f ∉ P.edge ∧ e ≠ f ∧ C.rotate (C.idxOf u) = WList.cons u e (P.concat f u)

theorem Graph.IsCyclicWalk.exists_isPath_edge {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) (hnt : C.Nontrivial) (he : e ∈ C.edge) : ∃ (n : ℕ) (P : WList α β), G.IsPath P ∧ e ∉ P.edge ∧ C.rotate n = WList.cons P.last e P

theorem Graph.IsCyclicWalk.loop_or_nontrivial {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) : (∃ (x : α) (e : β), C = WList.cons x e (WList.nil x)) ∨ C.Nontrivial

theorem Graph.IsCyclicWalk.toGraph_deleteVerts_first_eq {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) (hnt : C.Nontrivial) : C.toGraph.deleteVerts {C.first} = C.tail.dropLast.toGraph

theorem Graph.IsCyclicWalk.nontrivial_iff_vertexSet_nontrivial {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) : C.Nontrivial ↔ C.vertexSet.Nontrivial

theorem Graph.IsCyclicWalk.nontrivial_iff_edgeSet_nontrivial {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) : C.Nontrivial ↔ C.edgeSet.Nontrivial

theorem Graph.IsCyclicWalk.exists_isPath_toGraph_eq_delete_vertex {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) (hnt : C.Nontrivial) (hx : x ∈ C) : ∃ (P : WList α β), G.IsPath P ∧ P.toGraph = C.toGraph.deleteVerts {x}

Deleting a vertex from the graph of a nontrivial cycle gives the graph of a path.

theorem Graph.IsCyclicWalk.exists_isPath_toGraph_eq_delete_edge_of_isLink {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) (he : C.IsLink e x y) : ∃ (P : WList α β), G.IsPath P ∧ P.toGraph = C.toGraph.deleteEdges {e} ∧ P.first = x ∧ P.last = y

theorem Graph.IsCyclicWalk.exists_isPath_toGraph_eq_delete_edge {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) (heC : e ∈ C.edge) : ∃ (P : WList α β), G.IsPath P ∧ P.toGraph = C.toGraph.deleteEdges {e}

Deleting an edge from the graph of a cycle gives the graph of a path.

theorem Graph.IsPath.cons_isCyclicWalk {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) (he : G.IsLink e P.first P.last) (heP : e ∉ P.edge) : G.IsCyclicWalk (WList.cons P.last e P)

theorem Graph.IsPath.cons_isCyclicWalk_of_nontrivial {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) (he : G.IsLink e P.first P.last) (hPnt : P.Nontrivial) : G.IsCyclicWalk (WList.cons P.last e P)

If P is nontrivial, then the edge assumption from IsPath.cons_isCyclicWalk isn't needed.

theorem Graph.IsPath.concat_isCyclicWalk {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) (he : G.IsLink e P.last P.first) (heP : e ∉ P.edge) : G.IsCyclicWalk (P.concat e P.first)

Decompositions of cyclic walks

theorem Graph.IsCyclicWalk.isPath_of_mem_decomposeTo {α : Type u_1} {β : Type u_2} {G : Graph α β} {C P : WList α β} {L : List (WList α β)} [Inhabited α] (hC : G.IsCyclicWalk C) (hdec : C.DecomposeTo L) (hne : ∀ P ∈ L, P.Nonempty) (hcard : 1 < L.length) (hP : P ∈ L) : G.IsPath P

A member of a nontrivial decomposition of a cyclic walk is a path.

theorem Graph.IsCyclicWalk.map_first_nodup_of_decomposeTo {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} {L : List (WList α β)} [Inhabited α] (hC : G.IsCyclicWalk C) (hdec : C.DecomposeTo L) (hne : ∀ P ∈ L, P.Nonempty) : (List.map WList.first L).Nodup

The initial vertices of the pieces in a nonempty decomposition of a cyclic walk are distinct.

theorem Graph.IsCyclicWalk.pairwise_disjoint_internalVertexSet_of_decomposeTo {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} {L : List (WList α β)} [Inhabited α] (hC : G.IsCyclicWalk C) (hdec : C.DecomposeTo L) (hne : ∀ P ∈ L, P.Nonempty) : List.Pairwise (fun (P Q : WList α β) => Disjoint P.internalVertexSet Q.internalVertexSet) L

Distinct pieces in a nonempty decomposition of a cyclic walk have disjoint interiors.

theorem Graph.IsCyclicWalk.internalVertexSet_disjoint_map_first_of_decomposeTo {α : Type u_1} {β : Type u_2} {G : Graph α β} {C P : WList α β} {L : List (WList α β)} [Inhabited α] (hC : G.IsCyclicWalk C) (hdec : C.DecomposeTo L) (hne : ∀ P ∈ L, P.Nonempty) (hP : P ∈ L) : Disjoint P.internalVertexSet {x : α | x ∈ List.map WList.first L}

No internal vertex of a piece in a nonempty cyclic decomposition is the initial vertex of another piece.