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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The terminal first-pair and second-triple bounds hold in every independent orientation of the original system.

  1. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.terminal_oriented_first_ball line 16
  2. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.terminal_oriented_second_ball line 49