OAI/Combinatorics/RamseyFive/Geometry/ConcretePivot.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SharpRamseyFive.ProjectiveIncidence.PivotContext line 14
2. abbrev OAI.SharpRamseyFive.ProjectiveIncidence.PivotTape line 17
3. abbrev OAI.SharpRamseyFive.ProjectiveIncidence.PivotMessage line 19
4. def OAI.SharpRamseyFive.ProjectiveIncidence.pivotLeft line 22
5. def OAI.SharpRamseyFive.ProjectiveIncidence.pivotRight line 25
6. lemma OAI.SharpRamseyFive.ProjectiveIncidence.pivot_inheritance line 30
7. abbrev OAI.SharpRamseyFive.ProjectiveIncidence.PivotTreeTape line 38
8. abbrev OAI.SharpRamseyFive.ProjectiveIncidence.PivotTreeMessage line 40
9. instance OAI.SharpRamseyFive.ProjectiveIncidence.pivotTreeTapeFintype line 44
10. instance OAI.SharpRamseyFive.ProjectiveIncidence.pivotTreeMessageFintype line 49
11. def OAI.SharpRamseyFive.ProjectiveIncidence.pivotTreeLaw line 56
12. def OAI.SharpRamseyFive.ProjectiveIncidence.pivotTreeEncoded line 63
13. def OAI.SharpRamseyFive.ProjectiveIncidence.pivotTreeRetained line 74
14. lemma OAI.SharpRamseyFive.ProjectiveIncidence.pivotTree_retained_nodes line 82