Proof of `A graph or its complement has diameter at most 3`
groundedproofs/Lax185574Proofs/ComplementDiameter.lean · lax-185574
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.
In the paper
- page 32 of this submission's paper
Description
If some two vertices , are not joined by a walk of length at
most in , then they are distinct, non-adjacent and have no common
neighbor. In Ḡ they are adjacent, and every other vertex is adjacent to
or to . So any two vertices are joined in Ḡ by a walk that goes
to or , possibly crosses the edge , and leaves again, of
length at most .