OAI/Combinatorics/Ramsey/CycleClique/DenseCycles.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CycleClique.cycle_from_dense_layer line 17
2. theorem OAI.CycleClique.contains_half_clique line 103
3. theorem OAI.CycleClique.triangle_free_card_bound line 116
4. theorem OAI.CycleClique.counterexample_contains_triangle line 161
5. theorem OAI.CycleClique.complete_isContained_iff_le_cliqueNum line 173
6. theorem OAI.CycleClique.counterexample_clique_bound line 192