OAI/Combinatorics/SharpRamsey/Marking/GoodIndices.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SharpLogRamsey.Selection.badIndicesline 14 - lemma
OAI.SharpLogRamsey.Selection.not_badIndicesline 20 - lemma
OAI.SharpLogRamsey.Selection.badIndices_update_selfline 28 - theorem
OAI.SharpLogRamsey.Selection.selected_bad_absorptionline 36 - theorem
OAI.SharpLogRamsey.Selection.badIndices_cardline 51