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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual three terminal configurations, including restrictions on both targets of every short path between starting representatives.

  1. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.terminal_starting_classification line 18