OAI/Combinatorics/RamseyFive/Geometry/GuardedNodeSent.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.ProjectiveIncidence.guardedNode_sent_valid line 16
  2. lemma OAI.SharpRamseyFive.ProjectiveIncidence.guardedNode_original_capture line 32
  3. abbrev OAI.SharpRamseyFive.ProjectiveIncidence.OrientedNodeTape line 57
  4. instance OAI.SharpRamseyFive.ProjectiveIncidence.orientedNodeTapeFintype line 61
  5. abbrev OAI.SharpRamseyFive.ProjectiveIncidence.OrientedNodeMessage line 66
  6. def OAI.SharpRamseyFive.ProjectiveIncidence.orientedNodeTapeLaw line 72
  7. def OAI.SharpRamseyFive.ProjectiveIncidence.reverseNodePair line 77
  8. def OAI.SharpRamseyFive.ProjectiveIncidence.orientedNodeDecoded line 81
  9. def OAI.SharpRamseyFive.ProjectiveIncidence.orientedNodeCost line 89
  10. def OAI.SharpRamseyFive.ProjectiveIncidence.orientedGuardedNodeEncoded line 98
  11. lemma OAI.SharpRamseyFive.ProjectiveIncidence.orientedGuardedNode_law line 114