def WList.betweenSets {α : Type u_1} {β : Type u_2} (w : WList α β) (S T : Set α) [DecidablePred fun (x : α) => x ∈ S] [DecidablePred fun (x : α) => x ∈ T] : WList α β

Equations

• w.betweenSets S T = (w.suffixFromLast fun (x : α) => x ∈ S).prefixUntil fun (x : α) => x ∈ T

@[simp]

theorem WList.betweenSets_isInfix {α : Type u_1} {β : Type u_2} (w : WList α β) (S T : Set α) [DecidablePred fun (x : α) => x ∈ S] [DecidablePred fun (x : α) => x ∈ T] : (w.betweenSets S T).IsInfix w

theorem WList.betweenSets_first_mem_iff {α : Type u_1} {β : Type u_2} (w : WList α β) (S T : Set α) [DecidablePred fun (x : α) => x ∈ S] [DecidablePred fun (x : α) => x ∈ T] : (w.betweenSets S T).first ∈ S ↔ ∃ x ∈ w, x ∈ S

theorem WList.betweenSets_first_mem {α : Type u_1} {β : Type u_2} {w : WList α β} {S T : Set α} [DecidablePred fun (x : α) => x ∈ S] [DecidablePred fun (x : α) => x ∈ T] (hw : ∃ x ∈ w, x ∈ S) : (w.betweenSets S T).first ∈ S

theorem WList.betweenSets_first_eq_of_mem {α : Type u_1} {β : Type u_2} {v : α} {w : WList α β} {S T : Set α} [DecidablePred fun (x : α) => x ∈ S] [DecidablePred fun (x : α) => x ∈ T] (hv : v ∈ w.betweenSets S T) (hvS : v ∈ S) : (w.betweenSets S T).first = v

theorem WList.betweenSets_first_eq_iff_mem {α : Type u_1} {β : Type u_2} {v : α} {w : WList α β} {S T : Set α} [DecidablePred fun (x : α) => x ∈ S] [DecidablePred fun (x : α) => x ∈ T] (hw : ∃ x ∈ w, x ∈ S) : (w.betweenSets S T).first = v ↔ v ∈ (w.betweenSets S T).vertexSet ∧ v ∈ S

theorem WList.betweenSets_vertex_tail_not_prop {α : Type u_1} {β : Type u_2} (w : WList α β) (S T : Set α) [DecidablePred fun (x : α) => x ∈ S] [DecidablePred fun (x : α) => x ∈ T] (x : α) : x ∈ (w.betweenSets S T).vertex.tail → x ∉ S

theorem WList.betweenSets_last_mem {α : Type u_1} {β : Type u_2} {w : WList α β} {S T : Set α} [DecidablePred fun (x : α) => x ∈ S] [DecidablePred fun (x : α) => x ∈ T] (hw : ∃ u ∈ w.suffixFromLast fun (x : α) => x ∈ S, u ∈ T) : (w.betweenSets S T).last ∈ T

theorem WList.betweenSets_last_eq_of_mem {α : Type u_1} {β : Type u_2} {v : α} {w : WList α β} {S T : Set α} [DecidablePred fun (x : α) => x ∈ S] [DecidablePred fun (x : α) => x ∈ T] (hv : v ∈ w.betweenSets S T) (hvT : v ∈ T) : (w.betweenSets S T).last = v

theorem WList.betweenSets_last_eq_iff_mem {α : Type u_1} {β : Type u_2} {v : α} {w : WList α β} {S T : Set α} [DecidablePred fun (x : α) => x ∈ S] [DecidablePred fun (x : α) => x ∈ T] (hw : ∃ u ∈ w.suffixFromLast fun (x : α) => x ∈ S, u ∈ T) : (w.betweenSets S T).last = v ↔ v ∈ (w.betweenSets S T).vertexSet ∧ v ∈ T

theorem WList.betweenSets_vertex_dropLast_not_prop {α : Type u_1} {β : Type u_2} (w : WList α β) (S T : Set α) [DecidablePred fun (x : α) => x ∈ S] [DecidablePred fun (x : α) => x ∈ T] (x : α) : x ∈ (w.betweenSets S T).vertex.dropLast → x ∉ T

theorem WList.betweenSets_isPrefix_iff {α : Type u_1} {β : Type u_2} {w : WList α β} (S T : Set α) [DecidablePred fun (x : α) => x ∈ S] [DecidablePred fun (x : α) => x ∈ T] (hnd : w.vertex.Nodup) : (w.betweenSets S T).IsPrefix w ↔ ∀ x ∈ w.vertex.tail, x ∉ S

def WList.breakAt_aux {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] (e' : β) (w' : WList α β) (L : List (WList α β)) : List (WList α β)

Equations

• (WList.nil x).breakAt_aux P e' w' L = if P x then WList.nil x :: WList.cons x e' w' :: L else WList.cons x e' w' :: L
• (WList.cons x e w_2).breakAt_aux P e' w' L = if P x then w_2.breakAt_aux P e (WList.nil x) (WList.cons x e' w' :: L) else w_2.breakAt_aux P e (WList.cons x e' w') L

@[simp]

theorem WList.breakAt_aux_length {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] (e' : β) (w' : WList α β) (L : List (WList α β)) : (w.breakAt_aux P e' w' L).length = List.countP (fun (b : α) => decide (P b)) w.vertex + L.length + 1

theorem WList.breakAt_aux_append {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] (e' : β) (w' : WList α β) (L : List (WList α β)) : w.breakAt_aux P e' w' L = w.breakAt_aux P e' w' [] ++ L

theorem WList.breakAt_aux_eq_concat {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] (e' : β) (w' w'' : WList α β) : w.breakAt_aux P e' w' [w''] = (w.breakAt_aux P e' w' []).concat w''

@[simp]

theorem WList.breakAt_aux_foldl {α : Type u_1} {β : Type u_2} {x : α} (w : WList α β) (P : α → Prop) [DecidablePred P] (e' : β) (w' : WList α β) : List.foldl (fun (x1 x2 : WList α β) => x1 ++ x2) (nil x) (w.breakAt_aux P e' w' []) = w.reverse.concat e' w'.first ++ w'

theorem WList.breakAt_aux_ne_nil' {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] (e' : β) (w' : WList α β) : w.breakAt_aux P e' w' [] ≠ []

@[simp]

theorem WList.breakAt_aux_ne_nil {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] (e' : β) (w' : WList α β) (L : List (WList α β)) : w.breakAt_aux P e' w' L ≠ []

theorem WList.breakAt_aux_getLast {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] (e' : β) (w' : WList α β) : (w.breakAt_aux P e' w' []).getLast ⋯ = (w.prefixUntil P).reverse ++ cons w.first e' w'

theorem WList.breakAt_aux_head {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] (e' : β) (w' : WList α β) : (w.breakAt_aux P e' w' []).head ⋯ = if (w.vertex.all fun (x : α) => decide ¬P x) = true then (w.suffixFromLast P).reverse ++ cons w.first e' w' else (w.suffixFromLast P).reverse

theorem WList.breakAt_aux_isChain_eq {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] {e' : β} {w' : WList α β} : List.IsChain (fun (x1 x2 : WList α β) => x1.last = x2.first) (w.breakAt_aux P e' w' [])

theorem WList.nonempty_of_mem_breakAt_aux_tail {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] {e' : β} {w' Q : WList α β} (hQ : Q ∈ (w.breakAt_aux P e' w' []).tail) : Q.Nonempty

theorem WList.breakAt_aux_map_first_eq_vertex_filter {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] {e' : β} {w' : WList α β} : List.map (fun (x : WList α β) => x.first) (w.breakAt_aux P e' w' []).tail = (List.filter (fun (b : α) => decide (P b)) w.vertex).reverse

def WList.breakAt {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : List (WList α β)

The segmentation of w breaks w at every vertex satisfying P and returns the list of segments. With the possible exception of the first and the last segment, all segments have the endpoints satisfying P. If P never occurs, this is [w]. If w.first satisfies P, then the first segment is nil w.first. Similarly, if w.last satisfies P, then the last segment is nil w.last.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WList.breakAt_nil {α : Type u_1} {β : Type u_2} {x : α} {P : α → Prop} [DecidablePred P] : (nil x).breakAt P = if P x then [nil x, nil x] else [nil x]

theorem WList.breakAt_reverse_ne_nil {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : w.reverse.breakAt P ≠ []

@[simp]

theorem WList.breakAt_ne_nil {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} [DecidablePred P] : w.breakAt P ≠ []

theorem WList.breakAt_reverse_length {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.reverse.breakAt P).length = List.countP (fun (b : α) => decide (P b)) w.vertex + 1

@[simp]

theorem WList.breakAt_length {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.breakAt P).length = List.countP (fun (b : α) => decide (P b)) w.vertex + 1

theorem WList.breakAt_reverse_foldl_append_cancel {α : Type u_1} {β : Type u_2} {x : α} (w : WList α β) (P : α → Prop) [DecidablePred P] : List.foldl (fun (x1 x2 : WList α β) => x1 ++ x2) (nil x) (w.reverse.breakAt P) = w.reverse

@[simp]

theorem WList.breakAt_foldl_append_cancel {α : Type u_1} {β : Type u_2} {x : α} (w : WList α β) (P : α → Prop) [DecidablePred P] : List.foldl (fun (x1 x2 : WList α β) => x1 ++ x2) (nil x) (w.breakAt P) = w

@[simp]

theorem WList.breakAt_appendList {α : Type u_1} {β : Type u_2} [Inhabited α] (w : WList α β) (P : α → Prop) [DecidablePred P] : w.breakAt P⁺ = w

theorem WList.breakAt_reverse_getLast {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.reverse.breakAt P).getLast ⋯ = (w.prefixUntil P).reverse

theorem WList.breakAt_getLast {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.breakAt P).getLast ⋯ = w.suffixFromLast P

theorem WList.breakAt_reverse_head {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.reverse.breakAt P).head ⋯ = (w.suffixFromLast P).reverse

@[simp]

theorem WList.breakAt_head {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.breakAt P).head ⋯ = w.prefixUntil P

theorem WList.breakAt_reverse_isChain_eq {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : List.IsChain (fun (x1 x2 : WList α β) => x1.last = x2.first) (w.reverse.breakAt P)

theorem WList.breakAt_isChain_eq {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : List.IsChain (fun (x1 x2 : WList α β) => x1.last = x2.first) (w.breakAt P)

@[simp]

theorem WList.decomposeTo_breakAt {α : Type u_1} {β : Type u_2} [Inhabited α] (w : WList α β) (P : α → Prop) [DecidablePred P] : w.DecomposeTo (w.breakAt P)

theorem WList.nonempty_of_mem_breakAt_dropLast_tail' {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] {Q : WList α β} (hQ : Q ∈ (w.reverse.breakAt P).dropLast.tail) : Q.Nonempty

theorem WList.nonempty_of_mem_breakAt_dropLast_tail {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] {Q : WList α β} (hQ : Q ∈ (w.breakAt P).dropLast.tail) : Q.Nonempty

theorem WList.breakAt_reverse_tail_map_first_eq_vertex_filter_reverse {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : List.map (fun (x : WList α β) => x.first) (w.reverse.breakAt P).tail = List.filter (fun (b : α) => decide (P b)) w.reverse.vertex

theorem WList.breakAt_tail_map_first_eq_vertex_filter {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : List.map first (w.breakAt P).tail = List.filter (fun (b : α) => decide (P b)) w.vertex

theorem WList.breakAt_tail_map_first_eq_inter {α : Type u_1} {β : Type u_2} (w : WList α β) (S : Set α) [DecidablePred fun (x : α) => x ∈ S] : {x : α | x ∈ List.map first (w.breakAt fun (x : α) => x ∈ S).tail} = w.vertexSet ∩ S

theorem WList.exists_infix_of_prop {α : Type u_1} {β : Type u_2} {w : WList α β} {p q : α → Prop} (hfirst : p w.first) (hlast : q w.last) : ∃ (w' : WList α β), w'.IsInfix w ∧ p w'.first ∧ q w'.last ∧ (∀ x ∈ w'.vertex.tail, ¬p x) ∧ ∀ x ∈ w'.vertex.dropLast, ¬q x

theorem WList.exists_infix_of_exists_prop {α : Type u_1} {β : Type u_2} {w : WList α β} {p q : α → Prop} (hp : ∃ x ∈ w, p x) (hq : ∃ x ∈ w, q x) : ∃ (w' : WList α β), w'.IsInfix w ∧ ((p w'.first ∧ q w'.last ∧ (∀ x ∈ w'.vertex.tail, ¬p x) ∧ ∀ x ∈ w'.vertex.dropLast, ¬q x) ∨ q w'.first ∧ p w'.last ∧ (∀ x ∈ w'.vertex.tail, ¬q x) ∧ ∀ x ∈ w'.vertex.dropLast, ¬p x)

theorem WList.exists_dInc_prop_not_prop {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} (hfirst : P w.first) (hlast : ¬P w.last) : ∃ (e : β) (x : α) (y : α), w.DInc e x y ∧ P x ∧ ¬P y

If a proposition P holds at the first vertex of w but not the last, then w has a directed edge e from x to y such that x satisfies P but y doesn't.

theorem WList.exists_dInc_not_prop_prop {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} (hfirst : ¬P w.first) (hlast : P w.last) : ∃ (e : β) (x : α) (y : α), w.DInc e x y ∧ ¬P x ∧ P y

theorem WList.exists_isLink_prop_not_prop {α : Type u_1} {β : Type u_2} {x y : α} {w : WList α β} {P : α → Prop} (hxw : x ∈ w.vertexSet) (hT : P x) (hyw : y ∈ w.vertexSet) (hF : ¬P y) : ∃ (e : β) (x : α) (y : α), w.IsLink e x y ∧ P x ∧ ¬P y