OAI/Combinatorics/RamseyFive/Geometry/OrientedPivotTree.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SharpRamseyFive.ProjectiveIncidence.OrientedPivotTape line 17
  2. abbrev OAI.SharpRamseyFive.ProjectiveIncidence.OrientedPivotMessage line 19
  3. instance OAI.SharpRamseyFive.ProjectiveIncidence.orientedPivotMessageFintype line 21
  4. def OAI.SharpRamseyFive.ProjectiveIncidence.orientedPivotLeft line 27
  5. def OAI.SharpRamseyFive.ProjectiveIncidence.orientedPivotRight line 30
  6. lemma OAI.SharpRamseyFive.ProjectiveIncidence.orientedPivot_inheritance line 34
  7. abbrev OAI.SharpRamseyFive.ProjectiveIncidence.OrientedPivotTreeTape line 41
  8. abbrev OAI.SharpRamseyFive.ProjectiveIncidence.OrientedPivotTreeMessage line 42
  9. instance OAI.SharpRamseyFive.ProjectiveIncidence.orientedPivotTreeTapeFintype line 46
  10. instance OAI.SharpRamseyFive.ProjectiveIncidence.orientedPivotTreeMessageFintype line 50
  11. def OAI.SharpRamseyFive.ProjectiveIncidence.orientedPivotTreeLaw line 56
  12. def OAI.SharpRamseyFive.ProjectiveIncidence.orientedPivotTreeEncoded line 61
  13. def OAI.SharpRamseyFive.ProjectiveIncidence.orientedPivotTreeRetained line 71
  14. lemma OAI.SharpRamseyFive.ProjectiveIncidence.orientedPivotTree_retained_nodes line 77