OAI/Combinatorics/Ramsey/CycleClique/Construction/CEConnectivity.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The external-ear consequence of connectivity after each vertex deletion.
- theorem
OAI.CycleClique.Construction.ce_external_earline 8