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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

No short outside path can join the two internal vertices of an old amount-two path: its detour would absorb that old assigned path.

  1. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.forbidden_amount_two_detour line 16