OAI/Combinatorics/SharpRamsey/Selection/MixedLoss.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpLogRamsey.Selection.Law.attach_leftline 14 - theorem
OAI.SharpLogRamsey.Selection.Law.mixed_lossline 22