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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

An interior representative has a successor that is not a representative.

  1. theorem OAI.CycleClique.Construction.RawPathSystem.representative_successor line 14
  2. theorem OAI.CycleClique.Construction.RawPathSystem.exists_two_outside_completed_representatives line 50