Proof of `Combining recursive answers in round-or-cut` (1st statement)
groundedproofs/Lax263307Proofs/RecursiveRounding.lean · lax-263307
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
An edge cannot connect different parts of the partition. The selected sets inherit the disjointness of those parts, so their union's cardinality is the sum of their cardinalities.