OAI/Combinatorics/Ramsey/CycleClique/IndependenceTwo.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.CycleClique.alpha_two_adjline 11 - theorem
OAI.CycleClique.clique_ncard_le_cliqueNumline 32 - theorem
OAI.CycleClique.clique_of_anticomplete_vertexline 39 - theorem
OAI.CycleClique.connected_of_alpha_two_largeline 47 - theorem
OAI.CycleClique.deletion_connected_of_alpha_two_largeline 73 - theorem
OAI.CycleClique.degree_two_of_deletion_connectedline 135 - theorem
OAI.CycleClique.hamiltonian_of_alpha_twoline 176