Prescribed endpoint bags

PathDecomposition.EndsAt specifies the last bag, including the requirement that the decomposition has at least one bag. It is used in the induction for Fomin and Høie's endpoint-prescribed decomposition lemma. StartsAt specifies the first bag; reversing the order of bags exchanges the two endpoints.

def Algebraic.Cutwidth.PathDecomposition.EndsAt {W : Type} {H : SimpleGraph W} (D : PathDecomposition H) (X : Finset W) : Prop

The decomposition has a last bag, and that bag is exactly X.

Equations

• D.EndsAt X = ∃ (last : Fin D.length), (∀ (i : Fin D.length), i ≤ last) ∧ D.bag last = X

def Algebraic.Cutwidth.PathDecomposition.StartsAt {W : Type} {H : SimpleGraph W} (D : PathDecomposition H) (X : Finset W) : Prop

The decomposition has a first bag, and that bag is exactly X.

Equations

• D.StartsAt X = ∃ (first : Fin D.length), (∀ (i : Fin D.length), first ≤ i) ∧ D.bag first = X

def Algebraic.Cutwidth.PathDecomposition.reverse {W : Type} {H : SimpleGraph W} (D : PathDecomposition H) : PathDecomposition H

Reverse the order of all bags.

Equations

• D.reverse = { length := D.length, bag := fun (i : Fin D.length) => D.bag i.rev, vertex_mem := ⋯, edge_mem := ⋯, consecutive := ⋯ }

noncomputable def Algebraic.Cutwidth.PathDecomposition.relabel {W : Type} {H : SimpleGraph W} {V : Type} {G : SimpleGraph V} (D : PathDecomposition G) (e : G ≃g H) : PathDecomposition H

Relabel vertices along a graph isomorphism, preserving the bag indices.

Equations

• D.relabel e = { length := D.length, bag := fun (i : Fin D.length) => Finset.map e.toEmbedding (D.bag i), vertex_mem := ⋯, edge_mem := ⋯, consecutive := ⋯ }