OAI/Combinatorics/RamseyFive/Marking/TwoScan.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.Marking.swapFlag line 19
  2. lemma OAI.SharpRamseyFive.Marking.swapFlag_apply line 22
  3. def OAI.SharpRamseyFive.Marking.reverseTuple line 24
  4. lemma OAI.SharpRamseyFive.Marking.reverseTuple_consistent line 26
  5. lemma OAI.SharpRamseyFive.Marking.reverseTuple_incident line 32
  6. def OAI.SharpRamseyFive.Marking.reverseExpensive line 42
  7. lemma OAI.SharpRamseyFive.Marking.mem_reverseExpensive line 46
  8. lemma OAI.SharpRamseyFive.Marking.reverseExpensive_card line 56
  9. theorem OAI.SharpRamseyFive.Marking.unionExpensive_bound line 60
  10. def OAI.SharpRamseyFive.Marking.typedDomain line 87
  11. lemma OAI.SharpRamseyFive.Marking.typedDomain_subset line 95
  12. def OAI.SharpRamseyFive.Marking.finiteTypedDomain line 101
  13. def OAI.SharpRamseyFive.Marking.finitePopular line 105
  14. lemma OAI.SharpRamseyFive.Marking.finite_typed_decoding line 112
  15. lemma OAI.SharpRamseyFive.Marking.finiteTypedDomain_card line 126
  16. def OAI.SharpRamseyFive.Marking.twoScanTypes line 146
  17. def OAI.SharpRamseyFive.Marking.markingMessage line 150
  18. def OAI.SharpRamseyFive.Marking.forwardRecord line 154
  19. def OAI.SharpRamseyFive.Marking.backwardRecord line 157
  20. lemma OAI.SharpRamseyFive.Marking.forwardRecord_marking line 160
  21. lemma OAI.SharpRamseyFive.Marking.backwardRecord_marking line 168
  22. def OAI.SharpRamseyFive.Marking.forwardDomain line 177
  23. def OAI.SharpRamseyFive.Marking.backwardDomain line 180
  24. def OAI.SharpRamseyFive.Marking.markingDomain line 184
  25. lemma OAI.SharpRamseyFive.Marking.markingDomain_card line 190
  26. theorem OAI.SharpRamseyFive.Marking.marking_decodes line 198