Proof of `Independent sets lift and project through a blow-up` (4th statement)
groundedproofs/Lax263307Proofs/BlowUpIndependentSets.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
Projecting an independent set of copies gives an independent original set.
Proof strategy
If two projected vertices were adjacent, their selected representatives would be adjacent copies, contradicting independence.
Attribution
Bonnet–Chang, Section 6.