OAI/Combinatorics/Ramsey/CycleClique/LowerBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CycleClique.RamseyProperty.on_fintype line 10
2. def OAI.CycleClique.disjointCliques line 26
3. theorem OAI.CycleClique.disjointCliques_walk_fiber line 32
4. theorem OAI.CycleClique.disjointCliques_no_cycle line 39
5. theorem OAI.CycleClique.disjointCliques_no_compl_clique line 56
6. theorem OAI.CycleClique.ramsey_lower_counterexample line 70
7. theorem OAI.CycleClique.ramsey_property_lower_bound line 81