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

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Assigned-amount bookkeeping for the two actual representative surgeries.

  1. theorem OAI.CycleClique.Construction.RawPathSystem.exists_subchain_profile line 14
  2. theorem OAI.CycleClique.Construction.RawPathSystem.replacement_profiles_different line 22
  3. theorem OAI.CycleClique.Construction.RawPathSystem.replacement_profiles_same line 50
  4. theorem OAI.CycleClique.Construction.RawPathSystem.replace_different_chains_profiled line 88
  5. theorem OAI.CycleClique.Construction.RawPathSystem.replace_same_chain_profiled line 107