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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Manuscript grow:short: at least nine representatives force a short outside path, for every orientation of an optimal expanded system.

  1. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.short_representative_path line 15