OAI/Combinatorics/Ramsey/CycleClique/Construction/AssignedSubcollection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Every sublist of the assigned segments is realized by deleting its omitted segments.

  1. inductive OAI.CycleClique.Construction.SystemAssignedAmounts line 12
  2. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.exists_of_raw line 20
  3. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.append line 34
  4. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.sum_eq line 41
  5. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.length_eq line 49
  6. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.positive line 56
  7. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.cut line 67
  8. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.delete_one line 95
  9. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.realize_sublist_aux line 107
  10. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.realize_sublist line 124