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

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Elementary list surgery used to insert an outside detour in a chain.

  1. theorem OAI.CycleClique.Construction.chain_outside_interior line 8
  2. theorem OAI.CycleClique.Construction.chain_outside_interior_of_ne_nil line 18
  3. theorem OAI.CycleClique.Construction.reverse_join_chain line 29
  4. theorem OAI.CycleClique.Construction.nodup_insert_list line 40
  5. theorem OAI.CycleClique.Construction.chain_insert_between line 49
  6. theorem OAI.CycleClique.Construction.head_insert_between line 58
  7. theorem OAI.CycleClique.Construction.last_insert_between line 62