EndpointFullAttachment.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Rotating from a second attachment extends the prefix exclusion to every endpoint.

theorem OAI.CycleClique.Construction.spanningPath_first_tail_last line 8
theorem OAI.CycleClique.Construction.endpoint_attachment_of_prefix_preserved line 43

theorem OAI.CycleClique.Construction.full_endpoint_attachment line 75

Source documentation

Every endpoint has no neighbour outside the endpoint clique other than the one attachment vertex.

theorem full_endpoint_attachment {V : Type*} [Fintype V]
    {G : SimpleGraph V} {x : V} {W : Finset V} {r : ℕ}
    {f : Fin (r + 1) → V} (hf : IsSpanningPath G x W f) (t : Fin r)
    (hfinal : ∀ i : Fin (r + 1), f i ∈ pathEnds G x W r ↔ t.val < i.val)
    (hclique : G.IsClique (pathEnds G x W r : Set V))
    (hneighbors : ∀ e ∈ pathEnds G x W r, ∀ v, G.Adj e v → v ∈ W)
    (hsecond : ∃ w ∈ pathEnds G x W r,
      w ≠ f t.succ ∧ G.Adj (f t.castSucc) w) :
    ∀ w ∈ pathEnds G x W r, ∀ v, G.Adj w v →
      v ∈ pathEnds G x W r ∨ v = f t.castSucc := by
…

Mentions: OAI.CycleClique.Construction.IsSpanningPath, OAI.CycleClique.Construction.pathEnds