OAI/Combinatorics/SharpRamsey/Construction/InitialTools.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.Selection.uniformLaw line 15
2. lemma OAI.SharpLogRamsey.Selection.uniformLaw_event line 20
3. lemma OAI.SharpLogRamsey.Selection.uniformLaw_conditioned line 24
4. lemma OAI.SharpLogRamsey.rectangle_pair_iff line 37
5. def OAI.SharpLogRamsey.initial_context line 44
6. lemma OAI.SharpLogRamsey.independent_selected line 72
7. lemma OAI.SharpLogRamsey.selected_reverse_consistent line 86