OAI/Combinatorics/RamseyFive/Geometry/OrientedTreeDomains.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.ProjectiveIncidence.flagRectangle line 24
  2. lemma OAI.SharpRamseyFive.ProjectiveIncidence.mem_flagRectangle line 29
  3. def OAI.SharpRamseyFive.ProjectiveIncidence.orientedNodeDomain line 34
  4. def OAI.SharpRamseyFive.ProjectiveIncidence.orientedPublicDomain line 39
  5. theorem OAI.SharpRamseyFive.ProjectiveIncidence.orientedPublicDomain_card line 45
  6. lemma OAI.SharpRamseyFive.ProjectiveIncidence.targetCovered_some line 81
  7. theorem OAI.SharpRamseyFive.ProjectiveIncidence.orientedPublicDomain_coverage line 92
  8. abbrev OAI.SharpRamseyFive.ProjectiveIncidence.VariableTreeTape line 146
  9. def OAI.SharpRamseyFive.ProjectiveIncidence.variableTreeLaw line 148
  10. lemma OAI.SharpRamseyFive.ProjectiveIncidence.variableTreeLaw_eval line 152
  11. abbrev OAI.SharpRamseyFive.ProjectiveIncidence.VariableTreeMessage line 156
  12. def OAI.SharpRamseyFive.ProjectiveIncidence.variableTreeCost line 159
  13. lemma OAI.SharpRamseyFive.ProjectiveIncidence.variableTree_weight line 164
  14. def OAI.SharpRamseyFive.ProjectiveIncidence.variableTreeDomain line 173
  15. lemma OAI.SharpRamseyFive.ProjectiveIncidence.variableTreeDomain_valid line 181
  16. def OAI.SharpRamseyFive.ProjectiveIncidence.variableTreeEncoded line 187
  17. lemma OAI.SharpRamseyFive.ProjectiveIncidence.variableTreeDomain_card line 196
  18. lemma OAI.SharpRamseyFive.ProjectiveIncidence.variableTreeDomain_coverage line 215