OAI/Combinatorics/SharpRamsey/Marking/OrderedClassLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLogRamsey.Selection.Law.map_congr_support line 14
  2. def OAI.SharpLogRamsey.Selection.chosenOrder line 27
  3. lemma OAI.SharpLogRamsey.Selection.chosenOrder_mem line 31
  4. def OAI.SharpLogRamsey.Selection.orderedTuple line 37
  5. theorem OAI.SharpLogRamsey.Selection.ordered_cond_entropy line 43
  6. theorem OAI.SharpLogRamsey.Selection.ordered_deficit line 69
  7. lemma OAI.SharpLogRamsey.Selection.ordered_support line 85
  8. lemma OAI.SharpLogRamsey.Marking.scanConsistent_ordered line 107