OAI/Combinatorics/RamseyFive/Geometry/BaseSmallLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SharpRamseyFive.ScoreGeometry.baseSmallLaw line 17
2. theorem OAI.SharpRamseyFive.ScoreGeometry.eventually_two_law line 45
3. lemma OAI.SharpRamseyFive.ProjectiveIncidence.incident_mk_pair line 74
4. lemma OAI.SharpRamseyFive.ProjectiveIncidence.incident_coordinates line 81
5. lemma OAI.SharpRamseyFive.ProjectiveIncidence.incidences_coordinates line 90
6. lemma OAI.SharpRamseyFive.ProjectiveIncidence.decoded_coordinates line 99
7. def OAI.SharpRamseyFive.ProjectiveIncidence.bidualPoint line 127
8. lemma OAI.SharpRamseyFive.ProjectiveIncidence.incident_bidual line 130
9. lemma OAI.SharpRamseyFive.ProjectiveIncidence.incidences_bidual line 140