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

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Assigned amounts are uniquely determined by a chain and its clique.

  1. theorem OAI.CycleClique.Construction.outside_prefix_unique line 10
  2. theorem OAI.CycleClique.Construction.AssignedAmounts.equal_of_chain_eq line 33
  3. theorem OAI.CycleClique.Construction.AssignedAmounts.unique line 65
  4. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.equal_of_chains_eq line 73
  5. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.unique line 88