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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

At a representative cut, at most one old assigned path is absorbed. Its outside vertices are precisely the leading outside segment of the tail.

  1. structure OAI.CycleClique.Construction.AssignedCutProfile line 13
  2. theorem OAI.CycleClique.Construction.exists_assigned_cut_profile line 31