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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Manuscript grow:one for every pair of representatives of an oriented raw system with the optimal amount.

  1. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.representatives_one_exclusion line 16
  2. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.completed_representatives_one_exclusion line 56