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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The minimal-subcollection argument of terminal:increment. The graph realizations are explicit; the only arithmetic restriction is the proved five-case inequality for the amount excess.

  1. theorem OAI.CycleClique.Construction.ExpandedPathSystem.incident_le_twice_assignedCount line 17
  2. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.terminal_increment_weights line 27