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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Every optimal system is realized by a nonempty-chain raw system in exactly the canonical domain consumed by the finite certificates.

  1. theorem OAI.CycleClique.Construction.RawPathSystem.canonical_profile_nonempty line 14
  2. theorem OAI.CycleClique.Construction.ExpandedPathSystem.completeClique_chains_nonempty line 48
  3. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.exists_canonical_raw line 60