Joining rooted component partitions #
The completed pieces from disjoint components remain separate. Their remainders join through a new root; either that union is another completed piece or it is the new small remainder.
theorem
Algebraic.Cutwidth.Bisection.RedBlack.ConnectedPartition.Partial.part_subset
{V : Type}
{B : SimpleGraph V}
{S : Finset V}
{root : V}
{M : ℕ}
(Q : Partial B S root M)
{P : Finset V}
(member : P ∈ Q.parts)
:
P ⊆ S
theorem
Algebraic.Cutwidth.Bisection.RedBlack.ConnectedPartition.Partial.remainder_subset
{V : Type}
{B : SimpleGraph V}
{S : Finset V}
{root : V}
{M : ℕ}
(Q : Partial B S root M)
:
Q.remainder ⊆ S
theorem
Algebraic.Cutwidth.Bisection.RedBlack.ConnectedPartition.Internal.assemble
{V ι : Type}
[Fintype ι]
(B : SimpleGraph V)
(S : Finset V)
(root : V)
(M : ℕ)
(positive : 0 < M)
(region : ι → Finset V)
(regions : Pairwise fun (i j : ι) => Disjoint (region i) (region j))
(cover : insert root (Finset.univ.biUnion region) = S)
(excluded : ∀ (i : ι), root ∉ region i)
(count : Fintype.card ι ≤ 3)
(neighbor : ι → V)
(adjacent : ∀ (i : ι), B.Adj root (neighbor i))
(data : (i : ι) → Partial B (region i) (neighbor i) M)
: