Proof of `Anticomponent or complete blockade`
groundedproofs/Lax57Proofs/AnticomponentBlockade.lean · lax-57
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
Consider the connected components of the complement induced on . A component of size at least gives the first outcome. Otherwise, greedily group whole components into disjoint families, each of size at least . Distinct families are anticomplete in the complement and therefore complete in .