OAI/Combinatorics/SharpRamsey/Marking/MarkingCaps.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpLogRamsey.Marking.popularJoint_memline 16 - lemma
OAI.SharpLogRamsey.Marking.popularJoint_rank_posline 26 - lemma
OAI.SharpLogRamsey.Marking.popularJoint_first_cardline 41 - lemma
OAI.SharpLogRamsey.Marking.popularJoint_fiber_cardline 63 - lemma
OAI.SharpLogRamsey.Marking.cheapPopular_first_cardline 84 - lemma
OAI.SharpLogRamsey.Marking.cheapPopular_fiber_cardline 94 - lemma
OAI.SharpLogRamsey.Marking.cheapPopular_rank_posline 105 - lemma
OAI.SharpLogRamsey.Marking.cheapPoor_productline 116