Proof of `The independence number is at most the annihilation number`
groundedproofs/Lax421170Proofs/IndependenceBound.lean · lax-421170
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
Let be a maximum independent set, so . Since no edge has both endpoints in , every edge is incident to at most one vertex of , and hence . The smallest degrees sum to at most the degrees of any vertices, in particular of those in . Therefore , and by the maximality in the definition of .