OAI/Combinatorics/RamseyFive/Marking/ScanRecordPresent.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.Marking.scanRecord_present line 19
  2. theorem OAI.SharpRamseyFive.Marking.one_scan_entropy line 37
  3. def OAI.SharpRamseyFive.Marking.extendTuple line 71
  4. lemma OAI.SharpRamseyFive.Marking.extendTuple_at line 73
  5. abbrev OAI.SharpRamseyFive.Marking.FlagPair line 80
  6. def OAI.SharpRamseyFive.Marking.tupleFirst line 83
  7. def OAI.SharpRamseyFive.Marking.tupleSecond line 84
  8. def OAI.SharpRamseyFive.Marking.TupleConsistent line 86
  9. def OAI.SharpRamseyFive.Marking.TupleIncident line 89
  10. lemma OAI.SharpRamseyFive.Marking.tupleConsistent_extend line 92
  11. lemma OAI.SharpRamseyFive.Marking.tupleIncident_extend line 101
  12. def OAI.SharpRamseyFive.Marking.finiteRecord line 106
  13. def OAI.SharpRamseyFive.Marking.finiteRank line 109
  14. def OAI.SharpRamseyFive.Marking.expensiveSet line 112
  15. lemma OAI.SharpRamseyFive.Marking.finiteRecord_value line 116
  16. lemma OAI.SharpRamseyFive.Marking.expensiveSet_card line 122
  17. theorem OAI.SharpRamseyFive.Marking.expensiveSet_bound line 135
  18. def OAI.SharpRamseyFive.Marking.finiteDecodeRecord line 141
  19. def OAI.SharpRamseyFive.Marking.finiteDomain line 144
  20. lemma OAI.SharpRamseyFive.Marking.finite_decode line 149
  21. theorem OAI.SharpRamseyFive.Marking.finiteDomain_card line 158
  22. theorem OAI.SharpRamseyFive.Marking.finite_scan_decoding line 164