OAI/Combinatorics/SharpRamsey/Construction/InitialLaw.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.InitialExperiment.occupancyConstant line 19
2. lemma OAI.SharpLogRamsey.InitialExperiment.occupancyConstant_pos line 21
3. def OAI.SharpLogRamsey.InitialExperiment.goodEvent line 32
4. lemma OAI.SharpLogRamsey.InitialExperiment.goodEvent_half line 36
5. def OAI.SharpLogRamsey.InitialExperiment.law line 49
6. lemma OAI.SharpLogRamsey.InitialExperiment.law_dom line 52
7. def OAI.SharpLogRamsey.InitialExperiment.chosen line 62
8. lemma OAI.SharpLogRamsey.InitialExperiment.chosen_consistent line 65
9. def OAI.SharpLogRamsey.InitialExperiment.tuple line 68
10. lemma OAI.SharpLogRamsey.InitialExperiment.tuple_occurs line 71
11. lemma OAI.SharpLogRamsey.InitialExperiment.tuple_consistent line 77
12. lemma OAI.SharpLogRamsey.InitialExperiment.tuple_occupancy line 81
13. lemma OAI.SharpLogRamsey.InitialExperiment.alphabet_cap line 101