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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Each selected internal vertex is a representative in one orientation; vertices in different components may be oriented independently.

  1. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.profile_of_mem line 16
  2. theorem OAI.CycleClique.Construction.selectedChain_orientation line 29
  3. theorem OAI.CycleClique.Construction.RawPathSystem.representative_of_oriented_chain line 48
  4. theorem OAI.CycleClique.Construction.RawPathSystem.joint_orientation line 58