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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Singleton components of every orientation are exactly the missing clique vertices of the original expanded system.

  1. theorem OAI.CycleClique.Construction.ExpandedPathSystem.oriented_complete_singleton_iff line 14
  2. theorem OAI.CycleClique.Construction.ExpandedPathSystem.oriented_complete_tail_nil_iff line 41