def WList.concat {α : Type u_1} {β : Type u_2} : WList α β → β → α → WList α β

Add an edge and a vertex to the end of a WList

Equations

• (WList.nil x_3).concat x✝¹ x✝ = WList.cons x_3 x✝¹ (WList.nil x✝)
• (WList.cons x_3 e w).concat x✝¹ x✝ = WList.cons x_3 e (w.concat x✝¹ x✝)

@[simp]

theorem WList.concat_length {α : Type u_1} {β : Type u_2} {v : α} {e : β} {w : WList α β} : (w.concat e v).length = w.length + 1

inductive WList.TsiLw (α : Type u_3) (β : Type u_4) : Type (max u_3 u_4)

• nil {α : Type u_3} {β : Type u_4} (u : α) : TsiLw α β
• concat {α : Type u_3} {β : Type u_4} (w : TsiLw α β) (e : β) (u : α) : TsiLw α β

def WList.toWList {α : Type u_1} {β : Type u_2} : TsiLw α β → WList α β

Equations

• WList.toWList (WList.TsiLw.nil u) = WList.nil u
• WList.toWList (w.concat e u) = (WList.toWList w).concat e u

def WList.TsiLw.cons {α : Type u_1} {β : Type u_2} : α → β → TsiLw α β → TsiLw α β

Equations

• WList.TsiLw.cons x✝¹ x✝ (WList.TsiLw.nil u) = (WList.TsiLw.nil x✝¹).concat x✝ u
• WList.TsiLw.cons x✝¹ x✝ (w.concat e' u) = (WList.TsiLw.cons x✝¹ x✝ w).concat e' u

def WList.fromWList {α : Type u_1} {β : Type u_2} : WList α β → TsiLw α β

Equations

• (WList.nil u).fromWList = WList.TsiLw.nil u
• (WList.cons x_1 e w).fromWList = WList.TsiLw.cons x_1 e w.fromWList

@[simp]

theorem WList.concat_fromWList {α : Type u_1} {β : Type u_2} {u : α} {e : β} {w : WList α β} : (w.concat e u).fromWList = w.fromWList.concat e u

@[simp]

theorem WList.cons_toWList {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : TsiLw α β} : toWList (TsiLw.cons x e w) = cons x e (toWList w)

def WList.TsiLw_equiv {α : Type u_1} {β : Type u_2} : TsiLw α β ≃ WList α β

Equations

• WList.TsiLw_equiv = { toFun := fun (w : WList.TsiLw α β) => WList.toWList w, invFun := fun (w : WList α β) => w.fromWList, left_inv := ⋯, right_inv := ⋯ }

def WList.TsiLw.length {α : Type u_1} {β : Type u_2} : TsiLw α β → ℕ

Equations

• (WList.TsiLw.nil u).length = 0
• (w.concat e u).length = w.length + 1

@[simp]

theorem WList.TsiLw.length_cons {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : TsiLw α β} : (cons x e w).length = w.length + 1

@[simp]

theorem WList.TsiLw.length_fromWList {α : Type u_1} {β : Type u_2} {w : WList α β} : w.fromWList.length = w.length

@[simp]

theorem WList.TsiLw.length_toWList {α : Type u_1} {β : Type u_2} {w : TsiLw α β} : (toWList w).length = w.length

def WList.append {α : Type u_1} {β : Type u_2} : WList α β → WList α β → WList α β

Glue two wLists w₁, w₂ together. The last vertex of w₁ is ignored, so this is most reasonable if w₁.last = w₂.first

Equations

• (WList.nil _x).append x✝ = x✝
• (WList.cons x_2 e w).append x✝ = WList.cons x_2 e (w.append x✝)

@[instance_reducible]

instance WList.instAppend {α : Type u_1} {β : Type u_2} : Append (WList α β)

Equations

• WList.instAppend = { append := WList.append }

@[simp]

theorem WList.nil_concat {α : Type u_1} {β : Type u_2} {x y : α} {e : β} : (nil x).concat e y = cons x e (nil y)

Properties of concat operation

@[simp]

theorem WList.cons_concat {α : Type u_1} {β : Type u_2} {x y : α} {e f : β} {w : WList α β} : (cons x e w).concat f y = cons x e (w.concat f y)

@[simp]

theorem WList.concat_first {α : Type u_1} {β : Type u_2} {v : α} {e : β} {w : WList α β} : (w.concat e v).first = w.first

@[simp]

theorem WList.concat_last {α : Type u_1} {β : Type u_2} {v : α} {e : β} {w : WList α β} : (w.concat e v).last = v

@[simp]

theorem WList.concat_vertex {α : Type u_1} {β : Type u_2} {v : α} {e : β} {w : WList α β} : (w.concat e v).vertex = w.vertex ++ [v]

@[simp]

theorem WList.concat_edge {α : Type u_1} {β : Type u_2} {v : α} {e : β} {w : WList α β} : (w.concat e v).edge = w.edge ++ [e]

@[simp]

theorem WList.concat_edgeSet {α : Type u_1} {β : Type u_2} {v : α} {e : β} {w : WList α β} : (w.concat e v).edgeSet = insert e w.edgeSet

@[simp]

theorem WList.mem_concat {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} : x ∈ w.concat e y ↔ x ∈ w ∨ x = y

@[simp]

theorem WList.concat_nonempty {α : Type u_1} {β : Type u_2} (w : WList α β) (e : β) (x : α) : (w.concat e x).Nonempty

@[simp]

theorem WList.concat_vertexSet_eq {α : Type u_1} {β : Type u_2} (w : WList α β) (e : β) (x : α) : (w.concat e x).vertexSet = insert x w.vertexSet

@[simp]

theorem WList.idxOf_concat_of_mem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} [DecidableEq α] (hx : x ∈ w) : (w.concat e y).idxOf x = w.idxOf x

@[simp]

theorem WList.idxOf_concat_of_notMem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} [DecidableEq α] (hx : x ∉ w) : (w.concat e x).idxOf x = w.length + 1

theorem WList.idxOf_cons_concat_of_ne {α : Type u_1} {β : Type u_2} {u v : α} {e f : β} {w : WList α β} [DecidableEq α] (hvu : v ≠ u) (hv : v ∈ cons u e (w.concat f u)) : v ∈ w ∧ (cons u e (w.concat f u)).idxOf v = w.idxOf v + 1

theorem WList.get_concat {α : Type u_1} {β : Type u_2} (w : WList α β) (e : β) (x : α) {n : ℕ} (hn : n ≤ w.length) : (w.concat e x).get n = w.get n

theorem WList.dInc_concat {α : Type u_1} {β : Type u_2} (w : WList α β) (e : β) (x : α) : (w.concat e x).DInc e w.last x

theorem WList.DInc.concat {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.DInc e x y) (f : β) (v : α) : (w.concat f v).DInc e x y

theorem WList.dInc_concat_iff {α : Type u_1} {β : Type u_2} {u x y : α} {e f : β} {w : WList α β} : (w.concat f u).DInc e x y ↔ w.DInc e x y ∨ f = e ∧ x = w.last ∧ y = u

theorem WList.isLink_concat_iff {α : Type u_1} {β : Type u_2} {u x y : α} {e f : β} {w : WList α β} : (w.concat f u).IsLink e x y ↔ w.IsLink e x y ∨ f = e ∧ (x = w.last ∧ y = u ∨ x = u ∧ y = w.last)

theorem WList.concat_inj_left {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w₁ w₂ : WList α β} : w₁.concat e x = w₂.concat e x ↔ w₁ = w₂

theorem WList.concat_injective {α : Type u_1} {β : Type u_2} {x : α} {e : β} : Function.Injective fun (x_1 : WList α β) => x_1.concat e x

theorem WList.concat_inj_right {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} : w.concat e x = w.concat e y ↔ x = y

@[simp]

theorem WList.dIncFirst_concat_of_mem {α : Type u_1} {β : Type u_2} {x : α} {e f : β} [DecidableEq β] (w : WList α β) (he : e ∈ w.edge) : (w.concat f x).dIncFirst ⋯ = w.dIncFirst he

theorem WList.dIncFirst_concat {α : Type u_1} {β : Type u_2} {x : α} {e f : β} [DecidableEq β] (w : WList α β) (he : e ∈ (w.concat f x).edge) : (w.concat f x).dIncFirst he = if hew : e ∈ w.edge then w.dIncFirst hew else (w.last, x)

@[simp]

theorem WList.append_notation {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : w₁.append w₂ = w₁ ++ w₂

@[simp]

theorem WList.nil_append {α : Type u_1} {β : Type u_2} {x : α} {w₂ : WList α β} : nil x ++ w₂ = w₂

@[simp]

theorem WList.cons_append {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w₁ w₂ : WList α β} : cons x e w₁ ++ w₂ = cons x e (w₁ ++ w₂)

theorem WList.append_assoc {α : Type u_1} {β : Type u_2} (w₁ w₂ w₃ : WList α β) : w₁ ++ w₂ ++ w₃ = w₁ ++ (w₂ ++ w₃)

instance WList.instAssociativeHAppend {α : Type u_1} {β : Type u_2} : Std.Associative fun (x1 x2 : WList α β) => x1 ++ x2

@[simp]

theorem WList.append_vertex {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : (w₁ ++ w₂).vertex = w₁.vertex.dropLast ++ w₂.vertex

theorem WList.append_vertex' {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (heq : w₁.last = w₂.first) : (w₁ ++ w₂).vertex = w₁.vertex ++ w₂.vertex.tail

theorem WList.concat_eq_append {α : Type u_1} {β : Type u_2} (w : WList α β) (e : β) (x : α) : w.concat e x = w ++ cons w.last e (nil x)

@[simp]

theorem WList.concat_append {α : Type u_1} {β : Type u_2} (w₁ w₂ : WList α β) (e : β) (x : α) : w₁.concat e x ++ w₂ = w₁ ++ cons w₁.last e w₂

@[simp]

theorem WList.append_edge {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : (w₁ ++ w₂).edge = w₁.edge ++ w₂.edge

@[simp]

theorem WList.append_edgeSet {α : Type u_1} {β : Type u_2} (w₁ w₂ : WList α β) : (w₁ ++ w₂).edgeSet = w₁.edgeSet ∪ w₂.edgeSet

@[simp]

theorem WList.append_length {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : (w₁ ++ w₂).length = w₁.length + w₂.length

theorem WList.idxOf_append_right_of_notMem {α : Type u_1} {β : Type u_2} [DecidableEq α] {P Q : WList α β} {uf : α} (huf : uf ∉ P) : (P ++ Q).idxOf uf = P.length + Q.idxOf uf

@[simp]

theorem WList.append_nil {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (h : w.last = x) : w ++ nil x = w

@[simp]

theorem WList.append_first_of_eq {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.last = w₂.first) : (w₁ ++ w₂).first = w₁.first

@[simp]

theorem WList.append_first_of_nonempty {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.Nonempty) : (w₁ ++ w₂).first = w₁.first

@[simp]

theorem WList.append_last {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : (w₁ ++ w₂).last = w₂.last

@[simp]

theorem WList.append_concat {α : Type u_1} {β : Type u_2} (w₁ w₂ : WList α β) (e : β) (x : α) : w₁ ++ w₂.concat e x = (w₁ ++ w₂).concat e x

theorem WList.append_right_injective {α : Type u_1} {β : Type u_2} {w : WList α β} : Function.Injective fun (x : WList α β) => w ++ x

@[simp]

theorem WList.append_vertexSet_of_eq {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.last = w₂.first) : (w₁ ++ w₂).vertexSet = w₁.vertexSet ∪ w₂.vertexSet

theorem WList.edgeSet_disjoint_of_append_nodup {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : (w₁ ++ w₂).edge.Nodup) : Disjoint w₁.edgeSet w₂.edgeSet

theorem WList.mem_of_mem_append {α : Type u_1} {β : Type u_2} {x : α} {w₁ w₂ : WList α β} (hx : x ∈ w₁ ++ w₂) : x ∈ w₁ ∨ x ∈ w₂

@[simp]

theorem WList.mem_append_iff {α : Type u_1} {β : Type u_2} (w₁ w₂ : WList α β) (x : α) : x ∈ w₁ ++ w₂ ↔ x ∈ w₁.vertex.dropLast ∨ x ∈ w₂

@[simp]

theorem WList.mem_append_iff_of_eq {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.last = w₂.first) (x : α) : x ∈ w₁ ++ w₂ ↔ x ∈ w₁ ∨ x ∈ w₂

@[simp]

theorem WList.append_nonempty {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : (w₁ ++ w₂).Nonempty ↔ w₁.Nonempty ∨ w₂.Nonempty

@[simp]

theorem WList.append_right_inj_iff {α : Type u_1} {β : Type u_2} {w w₁ w₂ : WList α β} : w ++ w₁ = w ++ w₂ ↔ w₁ = w₂

@[simp]

theorem WList.append_right_eq_self {α : Type u_1} {β : Type u_2} {w w₁ : WList α β} : w ++ w₁ = w ↔ w₁ = nil w.last

@[simp]

theorem WList.append_left_eq_self {α : Type u_1} {β : Type u_2} {w w₁ : WList α β} : w₁ ++ w = w ↔ w₁.Nil

@[simp]

theorem WList.append_eq_nil_iff {α : Type u_1} {β : Type u_2} {x : α} {w₁ w₂ : WList α β} : w₁ ++ w₂ = nil x ↔ w₁.Nil ∧ w₂ = nil x

@[simp]

theorem WList.nil_append_iff {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : (w₁ ++ w₂).Nil ↔ w₁.Nil ∧ w₂.Nil

theorem WList.eq_append_of_vertex_mem {α : Type u_1} {β : Type u_2} {w : WList α β} {u : α} (hmem : u ∈ w) : ∃ (w₁ : WList α β) (w₂ : WList α β), w = w₁ ++ w₂ ∧ w₁.last = u ∧ w₂.first = u

See prefixUntilVertex_append_suffixFromVertex. The u ∈ w assumption isn't needed.

theorem WList.eq_append_cons_of_edge_mem {α : Type u_1} {β : Type u_2} {w : WList α β} {e : β} (he : e ∈ w.edge) : ∃ (w₁ : WList α β) (w₂ : WList α β), w = w₁ ++ cons w₁.last e w₂ ∧ e ∉ w₁.edge

theorem WList.append_dInc_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w₁ w₂ : WList α β} (h : w₁.last = w₂.first) : (w₁ ++ w₂).DInc e x y ↔ w₁.DInc e x y ∨ w₂.DInc e x y

theorem WList.append_isLink_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w₁ w₂ : WList α β} (h : w₁.last = w₂.first) : (w₁ ++ w₂).IsLink e x y ↔ w₁.IsLink e x y ∨ w₂.IsLink e x y

def WList.reverse {α : Type u_1} {β : Type u_2} : WList α β → WList α β

Reverse the order of the vertices and edges of a wList.

Equations

• (WList.nil u).reverse = WList.nil u
• (WList.cons x_1 e w).reverse = w.reverse.concat e x_1

@[simp]

theorem WList.reverse_nil {α : Type u_1} {β : Type u_2} {x : α} : (nil x).reverse = nil x

Properties of reverse operation

@[simp]

theorem WList.reverse_cons {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} : (cons x e w).reverse = w.reverse.concat e x

@[simp]

theorem WList.reverse_nonempty {α : Type u_1} {β : Type u_2} {w : WList α β} : w.reverse.Nonempty ↔ w.Nonempty

theorem WList.Nonempty.reverse {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) : w.reverse.Nonempty

@[simp]

theorem WList.reverse_nil_iff {α : Type u_1} {β : Type u_2} (w : WList α β) : w.reverse.Nil ↔ w.Nil

@[simp]

theorem WList.reverse_first {α : Type u_1} {β : Type u_2} {w : WList α β} : w.reverse.first = w.last

@[simp]

theorem WList.reverse_last {α : Type u_1} {β : Type u_2} {w : WList α β} : w.reverse.last = w.first

@[simp]

theorem WList.reverse_vertex {α : Type u_1} {β : Type u_2} {w : WList α β} : w.reverse.vertex = w.vertex.reverse

@[simp]

theorem WList.reverse_edge {α : Type u_1} {β : Type u_2} {w : WList α β} : w.reverse.edge = w.edge.reverse

@[simp]

theorem WList.reverse_edgeSet {α : Type u_1} {β : Type u_2} {w : WList α β} : w.reverse.edgeSet = w.edgeSet

@[simp]

theorem WList.reverse_length {α : Type u_1} {β : Type u_2} {w : WList α β} : w.reverse.length = w.length

theorem WList.reverse_append {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h_eq : w₁.last = w₂.first) : (w₁ ++ w₂).reverse = w₂.reverse ++ w₁.reverse

@[simp]

theorem WList.concat_reverse {α : Type u_1} {β : Type u_2} (w : WList α β) (e : β) (x : α) : (w.concat e x).reverse = cons x e w.reverse

@[simp]

theorem WList.zip_reverse {α : Type u_1} {β : Type u_2} (a : List α) (b : List β) (h : b.length + 1 = a.length) : (WList.zip a b h).reverse = WList.zip a.reverse b.reverse ⋯

theorem WList.Nonempty.firstEdge_concat {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} (hw : w.Nonempty) : firstEdge (w.concat e x) ⋯ = firstEdge w hw

@[simp]

theorem WList.reverse_reverse {α : Type u_1} {β : Type u_2} (w : WList α β) : w.reverse.reverse = w

theorem WList.reverse_inj {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.reverse = w₂.reverse) : w₁ = w₂

@[simp]

theorem WList.reverse_inj_iff {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : w₁.reverse = w₂.reverse ↔ w₁ = w₂

@[simp]

theorem WList.reverse_injective {α : Type u_1} {β : Type u_2} : Function.Injective reverse

theorem WList.reverse_eq_comm {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : w₁.reverse = w₂ ↔ w₁ = w₂.reverse

@[simp]

theorem WList.reverse_nontrivial_iff {α : Type u_1} {β : Type u_2} {w : WList α β} : w.reverse.Nontrivial ↔ w.Nontrivial

theorem WList.Nontrivial.reverse {α : Type u_1} {β : Type u_2} {w : WList α β} : w.Nontrivial → w.reverse.Nontrivial

Alias of the reverse direction of WList.reverse_nontrivial_iff.

@[simp]

theorem WList.mem_reverse {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} : x ∈ w.reverse ↔ x ∈ w

@[simp]

theorem WList.reverse_vertexSet {α : Type u_1} {β : Type u_2} (w : WList α β) : w.reverse.vertexSet = w.vertexSet

theorem WList.DInc.reverse {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.DInc e x y) : w.reverse.DInc e y x

@[simp]

theorem WList.dInc_reverse_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} : w.reverse.DInc e x y ↔ w.DInc e y x

theorem WList.dInc_iff_eq_of_dInc_of_vertex_nodup_right {α : Type u_1} {β : Type u_2} {u v x : α} {e f : β} {w : WList α β} (hw : w.vertex.Nodup) (hv : w.DInc e u v) : w.DInc f x v ↔ f = e ∧ x = u

theorem WList.DInc.left_mem_vertex_dropLast {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.DInc e x y) : x ∈ w.vertex.dropLast

@[simp]

theorem WList.isLink_reverse_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} : w.reverse.IsLink e x y ↔ w.IsLink e x y

theorem WList.concat_induction {α : Type u_1} {β : Type u_2} {motive : WList α β → Prop} (nil : ∀ (u : α), motive (nil u)) (concat : ∀ (w : WList α β) (e : β) (x : α), motive w → motive (w.concat e x)) (w : WList α β) : motive w

theorem WList.wellFormed_reverse_iff {α : Type u_1} {β : Type u_2} {w : WList α β} : w.reverse.WellFormed ↔ w.WellFormed

theorem WList.WellFormed.reverse {α : Type u_1} {β : Type u_2} {w : WList α β} : w.WellFormed → w.reverse.WellFormed

Alias of the reverse direction of WList.wellFormed_reverse_iff.

@[simp]

theorem WList.idxOf_reverse {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hw : w.vertex.Nodup) (hx : x ∈ w) : w.reverse.idxOf x = w.length - w.idxOf x

@[simp]

theorem WList.idxOf_reverse_add_idxOf {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hw : w.vertex.Nodup) (hx : x ∈ w) : w.reverse.idxOf x + w.idxOf x = w.length

@[simp]

theorem WList.idxOf_add_idxOf_reverse {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hw : w.vertex.Nodup) (hx : x ∈ w) : w.idxOf x + w.reverse.idxOf x = w.length

def WList.dIncLast {α : Type u_1} {β : Type u_2} [DecidableEq β] (w : WList α β) {e : β} (he : e ∈ w.edge) : α × α

Equations

• w.dIncLast he = (w.reverse.dIncFirst ⋯).swap

theorem WList.dIncLast_dInc {α : Type u_1} {β : Type u_2} [DecidableEq β] (w : WList α β) {e : β} (he : e ∈ w.edge) : w.DInc e (w.dIncLast he).1 (w.dIncLast he).2

@[simp]

theorem WList.dIncLast_cons_of_mem {α : Type u_1} {β : Type u_2} {x : α} {f : β} [DecidableEq β] (w : WList α β) {e : β} (he : e ∈ w.edge) : (cons x f w).dIncLast ⋯ = w.dIncLast he

theorem WList.dIncLast_cons {α : Type u_1} {β : Type u_2} {x : α} {f : β} [DecidableEq β] (w : WList α β) {e : β} (he : e ∈ (cons x f w).edge) : (cons x f w).dIncLast he = if hew : e ∈ w.edge then w.dIncLast hew else (x, w.first)

def WList.Nonempty.lastEdge {α : Type u_1} {β : Type u_2} (w : WList α β) (hw : w.Nonempty) : β

The last edge of a nonempty WList

Equations

• WList.Nonempty.lastEdge w hw = WList.Nonempty.firstEdge w.reverse ⋯

@[simp]

theorem WList.Nonempty.firstEdge_reverse {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) : firstEdge w.reverse ⋯ = lastEdge w hw

theorem WList.Nonempty.lastEdge_cons {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} (hw : w.Nonempty) : lastEdge (WList.cons x e w) ⋯ = lastEdge w hw

@[simp]

theorem WList.lastEdge_concat {α : Type u_1} {β : Type u_2} (w : WList α β) (e : β) (x : α) : Nonempty.lastEdge (w.concat e x) ⋯ = e

@[simp]

theorem WList.Nonempty.lastEdge_mem {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) : lastEdge w hw ∈ w.edge

@[simp]

theorem WList.lastEdge_cons_cons {α : Type u_1} {β : Type u_2} {x y : α} {e f : β} {w : WList α β} : Nonempty.lastEdge (cons x e (cons y f w)) ⋯ = Nonempty.lastEdge (cons y f w) ⋯

@[simp]

theorem WList.lastEdge_cons_nil {α : Type u_1} {β : Type u_2} {x y : α} {e : β} : Nonempty.lastEdge (cons x e (nil y)) ⋯ = e

def WList.map {α : Type u_1} {β : Type u_2} {α' : Type u_3} (f : α → α') : WList α β → WList α' β

Equations

• WList.map f (WList.nil u) = WList.nil (f u)
• WList.map f (WList.cons x_1 e w) = WList.cons (f x_1) e (WList.map f w)

@[simp]

theorem WList.map_nil {α : Type u_1} {β : Type u_2} {x : α} {α' : Type u_3} (f : α → α') : map f (nil x) = nil (f x)

@[simp]

theorem WList.map_cons {α : Type u_1} {β : Type u_2} {α' : Type u_3} (f : α → α') (x : α) (e : β) (w : WList α β) : map f (cons x e w) = cons (f x) e (map f w)

@[simp]

theorem WList.map_concat {α : Type u_1} {β : Type u_2} {α' : Type u_3} (w : WList α β) (f : α → α') (e : β) (x : α) : map f (w.concat e x) = (map f w).concat e (f x)

@[simp]

theorem WList.map_append {α : Type u_1} {β : Type u_2} {α' : Type u_3} (w₁ w₂ : WList α β) (f : α → α') : map f (w₁ ++ w₂) = map f w₁ ++ map f w₂

@[simp]

theorem WList.map_reverse {α : Type u_1} {β : Type u_2} {α' : Type u_3} (w : WList α β) (f : α → α') : map f w.reverse = (map f w).reverse

@[simp]

theorem WList.map_first {α : Type u_1} {β : Type u_2} {α' : Type u_3} (w : WList α β) (f : α → α') : (map f w).first = f w.first

@[simp]

theorem WList.map_last {α : Type u_1} {β : Type u_2} {α' : Type u_3} (w : WList α β) (f : α → α') : (map f w).last = f w.last

@[simp]

theorem WList.map_vertex {α : Type u_1} {β : Type u_2} {α' : Type u_3} (w : WList α β) (f : α → α') : (map f w).vertex = List.map f w.vertex

@[simp]

theorem WList.map_invFunOn_map {α : Type u_1} {β : Type u_2} {α' : Type u_3} {f : α → α'} [Nonempty α] {s : Set α} {w : WList α' β} (hw : w.vertexSet ⊆ f '' s) : map f (map (Function.invFunOn f s) w) = w

@[simp]

theorem WList.mem_map_iff {α : Type u_1} {β : Type u_2} {α' : Type u_3} (w : WList α β) (f : α → α') (x : α') : x ∈ map f w ↔ ∃ y ∈ w, f y = x

@[simp]

theorem WList.map_edge {α : Type u_1} {β : Type u_2} {α' : Type u_3} (w : WList α β) (f : α → α') : (map f w).edge = w.edge

@[simp]

theorem WList.edgeSet_map {α : Type u_1} {β : Type u_2} {α' : Type u_3} (w : WList α β) (f : α → α') : (map f w).edgeSet = w.edgeSet

@[simp]

theorem WList.map_length {α : Type u_1} {β : Type u_2} {α' : Type u_3} (w : WList α β) (f : α → α') : (map f w).length = w.length

@[simp]

theorem WList.map_nonempty {α : Type u_1} {β : Type u_2} {α' : Type u_3} (w : WList α β) (f : α → α') : (map f w).Nonempty ↔ w.Nonempty

def WList.edgeMap {α : Type u_1} {β : Type u_2} {β' : Type u_4} (k : β → β') : WList α β → WList α β'

Equations

• WList.edgeMap k (WList.nil u) = WList.nil u
• WList.edgeMap k (WList.cons x_1 e w) = WList.cons x_1 (k e) (WList.edgeMap k w)

@[simp]

theorem WList.edgeMap_nil {α : Type u_1} {β : Type u_2} {β' : Type u_4} (k : β → β') (x : α) : edgeMap k (nil x) = nil x

@[simp]

theorem WList.edgeMap_cons {α : Type u_1} {β : Type u_2} {β' : Type u_4} (k : β → β') (x : α) (e : β) (w : WList α β) : edgeMap k (cons x e w) = cons x (k e) (edgeMap k w)

@[simp]

theorem WList.edgeMap_concat {α : Type u_1} {β : Type u_2} {β' : Type u_4} (w : WList α β) (k : β → β') (e : β) (x : α) : edgeMap k (w.concat e x) = (edgeMap k w).concat (k e) x

@[simp]

theorem WList.edgeMap_append {α : Type u_1} {β : Type u_2} {β' : Type u_4} (w₁ w₂ : WList α β) (k : β → β') : edgeMap k (w₁ ++ w₂) = edgeMap k w₁ ++ edgeMap k w₂

@[simp]

theorem WList.edgeMap_reverse {α : Type u_1} {β : Type u_2} {β' : Type u_4} (w : WList α β) (k : β → β') : edgeMap k w.reverse = (edgeMap k w).reverse

@[simp]

theorem WList.edgeMap_first {α : Type u_1} {β : Type u_2} {β' : Type u_4} (w : WList α β) (k : β → β') : (edgeMap k w).first = w.first

@[simp]

theorem WList.edgeMap_last {α : Type u_1} {β : Type u_2} {β' : Type u_4} (w : WList α β) (k : β → β') : (edgeMap k w).last = w.last

@[simp]

theorem WList.edgeMap_vertex {α : Type u_1} {β : Type u_2} {β' : Type u_4} (w : WList α β) (k : β → β') : (edgeMap k w).vertex = w.vertex

@[simp]

theorem WList.edgeMap_edge {α : Type u_1} {β : Type u_2} {β' : Type u_4} (w : WList α β) (k : β → β') : (edgeMap k w).edge = List.map k w.edge

@[simp]

theorem WList.edgeedgeSet_map {α : Type u_1} {β : Type u_2} {β' : Type u_4} (w : WList α β) (k : β → β') : (edgeMap k w).edgeSet = k '' w.edgeSet

@[simp]

theorem WList.edgeMap_length {α : Type u_1} {β : Type u_2} {β' : Type u_4} (w : WList α β) (k : β → β') : (edgeMap k w).length = w.length

@[simp]

theorem WList.map_edgeMap {α : Type u_1} {β : Type u_2} {α' : Type u_3} {β' : Type u_4} (w : WList α β) (f : α → α') (k : β → β') : map f (edgeMap k w) = edgeMap k (map f w)

@[simp]

theorem WList.mem_edgeMap {α : Type u_1} {β : Type u_2} {β' : Type u_4} (w : WList α β) (k : β → β') (x : α) : x ∈ edgeMap k w ↔ x ∈ w

@[simp]

theorem WList.edgeMap_nonempty {α : Type u_1} {β : Type u_2} {β' : Type u_4} (w : WList α β) (σ : β → β') : (edgeMap σ w).Nonempty ↔ w.Nonempty