Proof of `Independent blow-up classes are hereditary` (2nd statement)
groundedproofs/Lax263307Proofs/BlowUpClasses.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
The independent blow-up closure is closed under induced embeddings.
Proof strategy
Compose the induced embedding with the existing projection to the host graph. The embedding and projection both preserve and reflect adjacency.
Attribution
Bonnet–Chang, Lemma 16, with empty fibres allowed as in the weighted construction.