OAI/Combinatorics/SharpRamsey/Marking/ClassTransport.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLogRamsey.ReciprocalBands.reflected_integer_band line 11
2. lemma OAI.SharpLogRamsey.ReciprocalBands.reflected_open_band line 19
3. abbrev OAI.SharpLogRamsey.Marking.CovectorPair line 34
4. def OAI.SharpLogRamsey.Marking.covectorTuple line 36
5. def OAI.SharpLogRamsey.Marking.covectorDomain line 39
6. lemma OAI.SharpLogRamsey.Marking.covectorDomain_mem line 42
7. lemma OAI.SharpLogRamsey.Marking.covectorDomain_card line 46
8. lemma OAI.SharpLogRamsey.Marking.covectorDomain_first line 49
9. lemma OAI.SharpLogRamsey.Marking.covectorDomain_second line 54
10. lemma OAI.SharpLogRamsey.Marking.covectorTuple_consistent line 59
11. lemma OAI.SharpLogRamsey.Marking.covectorTuple_flag line 67
12. theorem OAI.SharpLogRamsey.Marking.covectorDomain_reciprocal line 79
13. lemma OAI.SharpLogRamsey.Marking.covectorTuple_entropy line 121