Tree components from an edge deficit #
The endpoint induction for subcubic path decompositions removes a tree component of the complement of the prescribed last bag. An edge deficit forces such a component; the degree-sum argument locates the deficit.
theorem
Algebraic.Cutwidth.PathDecomposition.Internal.exists_small_tree_component_of_edge_deficit
{W : Type}
[Fintype W]
(H : SimpleGraph W)
(M : ℕ)
(deficit : (M + 1) * H.edgeFinset.card < M * Fintype.card W)
:
∃ (C : H.ConnectedComponent), C.toSimpleGraph.IsTree ∧ Fintype.card ↥C ≤ M
theorem
Algebraic.Cutwidth.PathDecomposition.Internal.exists_tree_component_of_card_edgeFinset_lt
{W : Type}
[Fintype W]
(H : SimpleGraph W)
(hcard : H.edgeFinset.card < Fintype.card W)
:
∃ (C : H.ConnectedComponent), C.toSimpleGraph.IsTree
theorem
Algebraic.Cutwidth.PathDecomposition.Internal.complement_card_edges_lt
{W : Type}
[Fintype W]
(H : SimpleGraph W)
(X : Finset W)
(degree : ∀ (v : W), H.degree v ≤ 3)
(large : Fintype.card W < 3 * X.card)
(outside : ∀ v ∈ X, 2 ≤ (H.neighborFinset v \ X).card)
: