OAI/Combinatorics/RamseyFive/Geometry/BaseFinitePublic.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SharpRamseyFive.ScoreGeometry.BaseMessage line 14
2. abbrev OAI.SharpRamseyFive.ScoreGeometry.BaseTable line 16
3. def OAI.SharpRamseyFive.ScoreGeometry.baseTableLaw line 18
4. def OAI.SharpRamseyFive.ScoreGeometry.baseTableEncoded line 23
5. def OAI.SharpRamseyFive.ScoreGeometry.baseFiniteEncoded line 30
6. lemma OAI.SharpRamseyFive.ScoreGeometry.baseFinite_exact line 36
7. theorem OAI.SharpRamseyFive.ScoreGeometry.baseFinite_law line 44
8. lemma OAI.SharpRamseyFive.ScoreGeometry.baseFinite_header line 54
9. def OAI.SharpRamseyFive.ScoreGeometry.scoredEncoded line 68
10. lemma OAI.SharpRamseyFive.ScoreGeometry.scoredEncoded_exact line 79
11. lemma OAI.SharpRamseyFive.ScoreGeometry.scoredEncoded_law line 88
12. lemma OAI.SharpRamseyFive.ScoreGeometry.scoredEncoded_header line 97
13. abbrev OAI.SharpRamseyFive.ScoreGeometry.ScoreTable line 115
14. def OAI.SharpRamseyFive.ScoreGeometry.scoreTableLaw line 117
15. def OAI.SharpRamseyFive.ScoreGeometry.scoreFiniteEncoded line 122
16. lemma OAI.SharpRamseyFive.ScoreGeometry.scoreFinite_exact line 133
17. theorem OAI.SharpRamseyFive.ScoreGeometry.scoreFinite_law line 141