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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Terminal classification for every representative pair in every independent orientation of the completed path system.

  1. abbrev OAI.CycleClique.Construction.ExpandedPathSystem.TerminalAlternative line 15
  2. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.terminal_representative_classification line 23
  3. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.terminal_completed_classification line 82
  4. theorem OAI.CycleClique.Construction.ExpandedPathSystem.TerminalAlternative.parameter_unique line 99