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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Manuscript Proposition terminal:contradiction, conditional only on the published Chvátal–Erdős alpha-two Hamiltonicity input.

  1. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.terminal_contradiction line 17