def WList.edgeRemove {α : Type u_1} {β : Type u_2} (F : Set β) [DecidablePred fun (x : β) => x ∈ F] : WList α β → WList α β

Remove edges from a WList that belong to a given edge set F.

Equations

• WList.edgeRemove F (WList.nil x_1) = WList.nil x_1
• WList.edgeRemove F (WList.cons x_1 e w) = if e ∈ F then WList.edgeRemove F w else WList.cons x_1 e (WList.edgeRemove F w)

@[simp]

theorem WList.edgeRemove_nil {α : Type u_1} {β : Type u_2} {x : α} {F : Set β} [DecidablePred fun (x : β) => x ∈ F] : edgeRemove F (nil x) = nil x

theorem WList.edgeRemove_cons {α : Type u_1} {β : Type u_2} {F : Set β} [DecidablePred fun (x : β) => x ∈ F] (x : α) (e : β) (w : WList α β) : edgeRemove F (cons x e w) = if e ∈ F then edgeRemove F w else cons x e (edgeRemove F w)

@[simp]

theorem WList.edgeRemove_cons_of_mem {α : Type u_1} {β : Type u_2} {e : β} {F : Set β} [DecidablePred fun (x : β) => x ∈ F] (heF : e ∈ F) (x : α) (w : WList α β) : edgeRemove F (cons x e w) = edgeRemove F w

@[simp]

theorem WList.edgeRemove_cons_of_notMem {α : Type u_1} {β : Type u_2} {e : β} {F : Set β} [DecidablePred fun (x : β) => x ∈ F] (heF : e ∉ F) (x : α) (w : WList α β) : edgeRemove F (cons x e w) = cons x e (edgeRemove F w)

@[simp]

theorem WList.edgeRemove_empty {α : Type u_1} {β : Type u_2} (w : WList α β) : edgeRemove ∅ w = w

theorem WList.edgeRemove_notMem_edge {α : Type u_1} {β : Type u_2} {F : Set β} [DecidablePred fun (x : β) => x ∈ F] (w : WList α β) (e : β) (he : e ∈ F) : e ∉ (edgeRemove F w).edge

@[simp]

theorem WList.edgeRemove_edgeRemove {α : Type u_1} {β : Type u_2} (F F' : Set β) [DecidablePred fun (x : β) => x ∈ F] [DecidablePred fun (x : β) => x ∈ F'] [DecidablePred fun (x : β) => x ∈ F ∪ F'] (w : WList α β) : edgeRemove F' (edgeRemove F w) = edgeRemove (F ∪ F') w

@[simp]

theorem WList.edgeRemove_last {α : Type u_1} {β : Type u_2} {F : Set β} [DecidablePred fun (x : β) => x ∈ F] (w : WList α β) : (edgeRemove F w).last = w.last

@[simp]

theorem WList.edgeRemove_edge {α : Type u_1} {β : Type u_2} {F : Set β} [DecidablePred fun (x : β) => x ∈ F] (w : WList α β) : (edgeRemove F w).edge = List.filter (fun (x : β) => decide (x ∉ F)) w.edge

@[simp]

theorem WList.mem_edgeRemove_edge_iff {α : Type u_1} {β : Type u_2} {e : β} {F : Set β} {w : WList α β} [DecidablePred fun (x : β) => x ∈ F] : e ∈ (edgeRemove F w).edge ↔ e ∈ w.edge ∧ e ∉ F

@[simp]

theorem WList.edgeRemove_edgeSet {α : Type u_1} {β : Type u_2} {F : Set β} [DecidablePred fun (x : β) => x ∈ F] (w : WList α β) : (edgeRemove F w).edgeSet = w.edgeSet \ F

theorem WList.edgeRemove_append_eq_right {α : Type u_1} {β : Type u_2} {F : Set β} [DecidablePred fun (x : β) => x ∈ F] (w₁ w₂ : WList α β) (hw₁ : w₁.edgeSet ⊆ F) : edgeRemove F (w₁ ++ w₂) = edgeRemove F w₂

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

A WList has no loops if no edge connects a vertex to the next vertex being itself.

Equations

• (WList.nil x_1).NoLoop = True
• (WList.cons x_1 e w).NoLoop = (x_1 ≠ w.first ∧ w.NoLoop)

@[simp]

theorem WList.noLoop_nil {α : Type u_1} {β : Type u_2} (x : α) : (nil x).NoLoop

@[simp]

theorem WList.noLoop_cons {α : Type u_1} {β : Type u_2} (x : α) (e : β) (w : WList α β) : (cons x e w).NoLoop ↔ x ≠ w.first ∧ w.NoLoop

@[simp]

theorem WList.noLoop_of_vertex_nodup {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.vertex.Nodup) : w.NoLoop

theorem WList.noLoop_iff_ne_of_dInc {α : Type u_1} {β : Type u_2} {w : WList α β} : w.NoLoop ↔ ∀ (e : β) (x y : α), w.DInc e x y → x ≠ y

theorem WList.noLoop_iff_not_dInc {α : Type u_1} {β : Type u_2} {w : WList α β} : w.NoLoop ↔ ∀ (e : β) (x : α), ¬w.DInc e x x

@[simp]

theorem WList.NoLoop.not_dInc {α : Type u_1} {β : Type u_2} {w : WList α β} (h : w.NoLoop) (e : β) (x : α) : ¬w.DInc e x x

theorem WList.noLoop_iff_ne_of_isLink {α : Type u_1} {β : Type u_2} {w : WList α β} : w.NoLoop ↔ ∀ (e : β) (x y : α), w.IsLink e x y → x ≠ y

theorem WList.noLoop_iff_not_isLink {α : Type u_1} {β : Type u_2} {w : WList α β} : w.NoLoop ↔ ∀ (e : β) (x : α), ¬w.IsLink e x x

@[simp]

theorem WList.NoLoop.not_isLink {α : Type u_1} {β : Type u_2} {w : WList α β} (h : w.NoLoop) (e : β) (x : α) : ¬w.IsLink e x x

def WList.deloop {α : Type u_1} {β : Type u_2} [DecidableEq α] : WList α β → WList α β

Remove loops from a WList by removing edges where the source equals the target.

Equations

• (WList.nil x_1).deloop = WList.nil x_1
• (WList.cons x_1 e w).deloop = if x_1 = w.first then w.deloop else WList.cons x_1 e w.deloop

@[simp]

theorem WList.deloop_nil {α : Type u_1} {β : Type u_2} [DecidableEq α] (x : α) : (nil x).deloop = nil x

theorem WList.deloop_cons_eq_ite {α : Type u_1} {β : Type u_2} [DecidableEq α] (x : α) (e : β) (w : WList α β) : (cons x e w).deloop = if x = w.first then w.deloop else cons x e w.deloop

@[simp]

theorem WList.deloop_cons_of_eq_first {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hxw : x = w.first) (e : β) : (cons x e w).deloop = w.deloop

@[simp]

theorem WList.deloop_cons_of_ne_first {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hxw : x ≠ w.first) (e : β) : (cons x e w).deloop = cons x e w.deloop

@[simp]

theorem WList.deloop_first {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) : w.deloop.first = w.first

@[simp]

theorem WList.deloop_last {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) : w.deloop.last = w.last

theorem WList.deloop_isSublist {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) : w.deloop.IsSublist w

@[simp]

theorem WList.deloop_vertexSet {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) : w.deloop.vertexSet = w.vertexSet

@[simp]

theorem WList.mem_deloop_iff {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] : x ∈ w.deloop ↔ x ∈ w

theorem WList.deloop_isSublist_mono {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} [DecidableEq α] (h : w₁.IsSublist w₂) : w₁.deloop.IsSublist w₂.deloop

theorem WList.deloop_noLoop {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) : w.deloop.NoLoop

@[simp]

theorem WList.deloop_eq_self {α : Type u_1} {β : Type u_2} {w : WList α β} [DecidableEq α] (hw : w.NoLoop) : w.deloop = w

@[simp]

theorem WList.deloop_eq_self_iff {α : Type u_1} {β : Type u_2} {w : WList α β} [DecidableEq α] : w.deloop = w ↔ w.NoLoop