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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Recover the lower bound on every original assigned amount from an actual classified short path between completed representatives.

  1. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.minimum_of_subset line 16
  2. theorem OAI.CycleClique.Construction.chainRepresentatives_clique_head line 33
  3. theorem OAI.CycleClique.Construction.ExpandedPathSystem.complete_tail_nil_iff line 47
  4. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.terminal_completed_profile_minimum line 52