OAI/Combinatorics/SharpRamsey/Selection/HistoryLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpLogRamsey.Selection.Law.sigma line 13
  2. lemma OAI.SharpLogRamsey.Selection.Law.sigma_sum line 27
  3. lemma OAI.SharpLogRamsey.Selection.Law.history_sum line 32
  4. lemma OAI.SharpLogRamsey.Selection.Law.nullFree_map line 37
  5. abbrev OAI.SharpLogRamsey.Selection.Law.History line 44
  6. abbrev OAI.SharpLogRamsey.Selection.Law.HistorySource line 46
  7. abbrev OAI.SharpLogRamsey.Selection.Law.HistoryExtension line 49
  8. def OAI.SharpLogRamsey.Selection.Law.historyExtension line 52
  9. lemma OAI.SharpLogRamsey.Selection.Law.historyExtension_support line 57
  10. theorem OAI.SharpLogRamsey.Selection.Law.historyExtension_source line 62
  11. theorem OAI.SharpLogRamsey.Selection.Law.historyExtension_bound line 79