LeanPool.AsymptoticTrianglePacking.Internal — Module D2 : assembling the per-round matchings

Standalone, Mathlib-only. Foundation for the Rödl-nibble project.

The nibble builds its final matching as the union of the matchings produced in each round. Because each round works on the residual hypergraph (vertices not yet covered), the round matchings have pairwise-disjoint supports. This module proves the deterministic assembly facts:

• biUnion_isMatching — a family of matchings of H with pairwise-disjoint supports unions to a single matching of H.
• biUnion_card — if additionally all edges are nonempty (true for r ≥ 1), the union's size is the sum of the per-round sizes.

Definitions (IsMatching, support) come from LeanPool.AsymptoticTrianglePacking.Internal.Basic / LeanPool.AsymptoticTrianglePacking.Internal.Greedy. Must be placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].

theorem Hypergraph.support_union {V : Type u_1} [DecidableEq V] (M₁ M₂ : Finset (Finset V)) : support (M₁ ∪ M₂) = support M₁ ∪ support M₂

Support of a union is the union of supports.

theorem Hypergraph.subset_support {V : Type u_1} [DecidableEq V] {M : Finset (Finset V)} {e : Finset V} (he : e ∈ M) : e ⊆ support M

An edge of a family is contained in the family's support.

theorem Hypergraph.biUnion_isMatching {V : Type u_1} [DecidableEq V] {ι : Type u_2} {H : Finset (Finset V)} (T : Finset ι) (M : ι → Finset (Finset V)) (hM : ∀ i ∈ T, IsMatching H (M i)) (hdisj : ∀ i ∈ T, ∀ j ∈ T, i ≠ j → Disjoint (support (M i)) (support (M j))) : IsMatching H (T.biUnion M)

D2a — union of disjoint-support matchings is a matching.

theorem Hypergraph.biUnion_card {V : Type u_1} [DecidableEq V] {ι : Type u_2} {H : Finset (Finset V)} (T : Finset ι) (M : ι → Finset (Finset V)) (hM : ∀ i ∈ T, IsMatching H (M i)) (hne : ∀ e ∈ H, e.Nonempty) (hdisj : ∀ i ∈ T, ∀ j ∈ T, i ≠ j → Disjoint (support (M i)) (support (M j))) : (T.biUnion M).card = ∑ i ∈ T, (M i).card

D2b — the union's size is the sum of the per-round sizes (edges nonempty, e.g. r ≥ 1).