OAI/Combinatorics/IndependentSets/Reduction/ExtensionLaw.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LargeIndependentSets.extensionLaw line 13
2. lemma OAI.LargeIndependentSets.restriction_extensionLaw line 19
3. def OAI.LargeIndependentSets.embeddingInside line 31
4. lemma OAI.LargeIndependentSets.embeddingInside_trans line 39
5. lemma OAI.LargeIndependentSets.restriction_extensionLaw_inside line 46
6. def OAI.LargeIndependentSets.rationalExhaustion line 59
7. lemma OAI.LargeIndependentSets.rationalExhaustion_card line 62
8. lemma OAI.LargeIndependentSets.eventually_mem_rationalExhaustion line 65
9. lemma OAI.LargeIndependentSets.eventually_range_rationalExhaustion line 71
10. lemma OAI.LargeIndependentSets.finite_embedding_sorted line 75
11. def OAI.LargeIndependentSets.tailLarge line 85
12. lemma OAI.LargeIndependentSets.tailLarge_congr line 89
13. lemma OAI.LargeIndependentSets.tailLarge_color line 98
14. def OAI.LargeIndependentSets.RamseyInvariant line 108
15. lemma OAI.LargeIndependentSets.RamseyInvariant_empty line 111
16. lemma OAI.LargeIndependentSets.RamseyInvariant_extend line 118
17. lemma OAI.LargeIndependentSets.tailLarge_homogeneous line 163
18. theorem OAI.LargeIndependentSets.finite_homogeneous_of_infinite line 180
19. theorem OAI.LargeIndependentSets.finite_hypergraph_ramsey line 187
20. theorem OAI.LargeIndependentSets.finite_hypergraph_ramsey_subset line 227
21. theorem OAI.LargeIndependentSets.finite_simultaneous_ramsey line 267
22. theorem OAI.LargeIndependentSets.compact_simultaneous_ramsey line 294