The finite subset split needed for a doubling step

Every set of size at most twice a bound is a disjoint union of two subsets of size at most that bound. The statement includes zero bounds and arbitrary finite cardinalities; no power-of-two or ambient finiteness assumption is needed. The proof uses Mathlib's exact-cardinality subset existence theorem and finite-set difference.

theorem Algebraic.Cutwidth.Extractor.exists_union_of_card_le_two_mul {ι : Type u_1} [DecidableEq ι] (U : Finset ι) {k : ℕ} (size : U.card ≤ 2 * k) : ∃ (S : Finset ι) (T : Finset ι), S ⊆ U ∧ T ⊆ U ∧ Disjoint S T ∧ S ∪ T = U ∧ S.card ≤ k ∧ T.card ≤ k

A subset within twice the capacity splits into disjoint parts within one capacity each.