OAI/Combinatorics/SharpRamsey/Marking/FinalMarking.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.flagPair line 13
2. lemma OAI.SharpLogRamsey.flagPair_injective line 16
3. def OAI.SharpLogRamsey.flagPairEquiv line 22
4. instance OAI.SharpLogRamsey.flagFintype line 30
5. lemma OAI.SharpLogRamsey.actualFlag_card line 33
6. def OAI.SharpLogRamsey.reversedFlagPairs line 48
7. lemma OAI.SharpLogRamsey.reversedFlagPairs_injective line 53
8. theorem OAI.SharpLogRamsey.source_marking_upper line 62
9. theorem OAI.SharpLogRamsey.described_selection_bound line 100