OAI/Combinatorics/RamseyFive/Decoding/PublicTraining.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.GreedyTraining.publicRegion line 14
2. def OAI.SharpRamseyFive.GreedyTraining.publicOwn line 17
3. def OAI.SharpRamseyFive.GreedyTraining.greedyList line 22
4. lemma OAI.SharpRamseyFive.GreedyTraining.firstIndex_greedyList line 25
5. lemma OAI.SharpRamseyFive.GreedyTraining.region_cell line 46
6. lemma OAI.SharpRamseyFive.GreedyTraining.clipped_publicOwn line 60
7. lemma OAI.SharpRamseyFive.GreedyTraining.ownCell_subset_publicOwn line 72
8. def OAI.SharpRamseyFive.GreedyTraining.twoPublicOwn line 91
9. theorem OAI.SharpRamseyFive.GreedyTraining.literal_cell_data line 94
10. lemma OAI.SharpRamseyFive.GreedyTraining.public_own_count line 125
11. lemma OAI.SharpRamseyFive.GreedyTraining.literal_small_own line 139