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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Expand one certified outside connector inside an explicit chain template. All old vertices are checked as a finite disjoint path collection.

  1. theorem OAI.CycleClique.Construction.RawPathSystem.expand_outside_template line 16