OAI/Combinatorics/RamseyFive/Decoding/LargeValueCount.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpRamseyFive.PencilRegularity.large_value_countline 12 - theorem
OAI.SharpRamseyFive.PencilRegularity.clipped_pencil_countline 32 - theorem
OAI.SharpRamseyFive.PencilRegularity.family_irregular_countline 50