OAI/Combinatorics/Ramsey/CycleClique/InducedGraphs.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CycleClique.indep_induce_iff_image line 12
2. theorem OAI.CycleClique.independence_induce_image line 22
3. theorem OAI.CycleClique.independence_add_le line 50
4. theorem OAI.CycleClique.clique_of_independence_le_one line 69
5. theorem OAI.CycleClique.bipartite_card_le_twice_indep line 86
6. theorem OAI.CycleClique.closedNeighborhood_singleton_card line 108