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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Degree bounds when two deleted vertices are the only neighbours outside the longest path.

  1. theorem OAI.CycleClique.Construction.endpoint_neighbor_card_le line 8
  2. theorem OAI.CycleClique.Construction.endpoint_degree_le_card_add_two line 41