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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Cut two different chains before their representatives and reconnect through a new outside path, retaining every old vertex.

  1. theorem OAI.CycleClique.Construction.RawPathSystem.amount_union line 14
  2. theorem OAI.CycleClique.Construction.RawPathSystem.replace_different_chains line 34
  3. theorem OAI.CycleClique.Construction.RawPathSystem.different_chain_count line 133