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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

An indexed path whose endpoints are adjacent can be started at any of its vertices.

  1. theorem OAI.CycleClique.Construction.cycleNext_eq_add_one line 9

    Distinct definitions of this name: OAI/Combinatorics/Ramsey/CycleClique/Construction/Shortening.lean:15 (different declaration text). Qualify references as OAI.CycleClique.Construction.cycleNext_eq_add_one@path.

  2. theorem OAI.CycleClique.Construction.indexedPath_closed_cycle line 18
  3. theorem OAI.CycleClique.Construction.indexedPath_closed_ending line 37