OAI/Combinatorics/SharpRamsey/Selection/SupportIncidence.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpLogRamsey.Selection.good_pairing_eq_eventline 14 - lemma
OAI.SharpLogRamsey.Selection.auxiliary_good_mixtureline 27 - theorem
OAI.SharpLogRamsey.Selection.actual_auxiliary_incidenceline 39 - lemma
OAI.SharpLogRamsey.Selection.pairing_reverseline 66 - theorem
OAI.SharpLogRamsey.Selection.actual_auxiliary_target_leftline 77 - theorem
OAI.SharpLogRamsey.Selection.actual_auxiliary_target_rightline 100