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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Amount profiles of actual path systems, including singleton components for unused clique vertices. No canonical ordering is assumed here.

  1. theorem OAI.CycleClique.Construction.exists_chain_profiles line 14
  2. theorem OAI.CycleClique.Construction.ChainProfiles.amount line 28
  3. theorem OAI.CycleClique.Construction.ChainProfiles.assignedCount line 39
  4. theorem OAI.CycleClique.Construction.ChainProfiles.vertices line 48
  5. theorem OAI.CycleClique.Construction.ChainProfiles.positive line 64
  6. theorem OAI.CycleClique.Construction.ExpandedPathSystem.exists_complete_profile line 81