Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Proof of `Independent sets lift and project through a blow-up` (1st statement)

groundedproofs/Lax263307Proofs/BlowUpIndependentSets.lean · lax-263307

What this proof establishes

no assumptions

thm✓Lax263307.BlowUpIndependentSets (1st statement)

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

The cardinality of a complete lift is the sum of the fibre sizes.

Proof strategy

Use the cardinality formula for a finite dependent sum and the cardinality of each FinFin fibre.

Attribution

Bonnet–Chang, Section 6.