OAI/Combinatorics/RamseyFive/Decoding/OffFiberPairs.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SharpRamseyFive.NondominantOverlap.offFiberPairsline 12 - lemma
OAI.SharpRamseyFive.NondominantOverlap.card_offFiberPairsline 16 - lemma
OAI.SharpRamseyFive.NondominantOverlap.offFiberPairs_manyline 21 - def
OAI.SharpRamseyFive.NondominantOverlap.onPlaneline 36 - def
OAI.SharpRamseyFive.NondominantOverlap.planePairsline 39 - lemma
OAI.SharpRamseyFive.NondominantOverlap.planePairs_disjointline 42 - theorem
OAI.SharpRamseyFive.NondominantOverlap.rich_nondominant_plane_countline 62