Counting boundary vertices and induced crossing edges

Charge each boundary vertex to an incident crossing edge. Boundary vertices on the same side cannot receive the same edge. Restricting to an induced graph preserves each crossing edge and cannot add new ones.

theorem Algebraic.Cutwidth.PathDecomposition.Internal.cutFinset_compl {W : Type} [Fintype W] (H : SimpleGraph W) (S : Finset W) : H.cutFinset Sᶜ = H.cutFinset S

theorem Algebraic.Cutwidth.PathDecomposition.Internal.card_cutBoundary_le {W : Type} [Fintype W] (H : SimpleGraph W) (S : Finset W) : (cutBoundary H S).card ≤ (H.cutFinset S).card

theorem Algebraic.Cutwidth.PathDecomposition.Internal.card_cutFinset_induce_le {W : Type} [Fintype W] (H : SimpleGraph W) (S : Finset W) (T : Set W) [DecidablePred fun (x : W) => x ∈ T] [Fintype ↑T] : ((SimpleGraph.induce T H).cutFinset (Finset.subtype (fun (x : W) => x ∈ T) S)).card ≤ (H.cutFinset S).card