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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Attachment conclusions restricted to neighbours in the longest path's vertex set.

  1. theorem OAI.CycleClique.Construction.endpoint_attachment_vertex_of_prefix_preserved line 8
  2. theorem OAI.CycleClique.Construction.partial_endpoint_attachment_in_W line 37
  3. theorem OAI.CycleClique.Construction.full_endpoint_attachment_in_W line 57