OAI/Combinatorics/RamseyFive/Marking/ClassifiedStream.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.Marking.DomainClass line 22
2. lemma OAI.SharpRamseyFive.Marking.classValid_domainClass line 31
3. lemma OAI.SharpRamseyFive.Marking.classStream_domainClass line 43
4. lemma OAI.SharpRamseyFive.Marking.classDomain_cap line 61
5. lemma OAI.SharpRamseyFive.Marking.classDomain_log_cap line 67
6. lemma OAI.SharpRamseyFive.Marking.classStream_occupancy line 78