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.

Read the Lean proof on GitHub

Description

Let SS be a maximum independent set, so ∣S∣=α(G)|S| = \alpha(G). Since no edge has both endpoints in SS, every edge is incident to at most one vertex of SS, and hence ∑v∈Sd(v)≤m\sum_{v \in S} d(v) \le m. The α(G)\alpha(G) smallest degrees sum to at most the degrees of any α(G)\alpha(G) vertices, in particular of those in SS. Therefore ∑i=1α(G)di≤m\sum_{i=1}^{\alpha(G)} d_i \le m, and α(G)≤a(G)\alpha(G) \le a(G) by the maximality in the definition of a(G)a(G).