OAI/Combinatorics/RamseyFive/Marking/MarkedStreamExtraction.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.Marking.markedContext line 23
2. def OAI.SharpRamseyFive.Marking.markedPositions line 26
3. def OAI.SharpRamseyFive.Marking.markedEvent line 31
4. def OAI.SharpRamseyFive.Marking.classStream line 35
5. lemma OAI.SharpRamseyFive.Marking.markedContext_law line 44
6. lemma OAI.SharpRamseyFive.Marking.actual_marked_class line 51
7. lemma OAI.SharpRamseyFive.Marking.classStream_density line 68
8. lemma OAI.SharpRamseyFive.Marking.classStream_joint line 81
9. lemma OAI.SharpRamseyFive.Marking.classStream_consistent line 102
10. def OAI.SharpRamseyFive.Marking.classDomain line 120
11. lemma OAI.SharpRamseyFive.Marking.marked_indices_properties line 128
12. lemma OAI.SharpRamseyFive.Marking.markedSelected_decodes line 139
13. lemma OAI.SharpRamseyFive.Marking.markedSelected_valid line 148
14. lemma OAI.SharpRamseyFive.Marking.classStream_tuple line 161
15. lemma OAI.SharpRamseyFive.Marking.classStream_event line 170
16. lemma OAI.SharpRamseyFive.Marking.classStream_contains line 180
17. lemma OAI.SharpRamseyFive.Marking.classStream_valid line 195