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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Deleting a set with one attachment preserves connectivity.

  1. theorem OAI.CycleClique.Construction.connected_outside_single_attachment line 8
  2. theorem OAI.CycleClique.Construction.neighbors_outside_single_attachment line 45
  3. theorem OAI.CycleClique.Construction.degree_outside_single_attachment line 52