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

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CycleClique.Construction.successor_closed_final_segment line 10

   Source documentation

   A nonempty successor-closed subset of a finite interval, excluding zero, starts immediately after a well-defined boundary index.

   theorem successor_closed_final_segment {r : ℕ} (P : Fin (r + 1) → Prop)
       (hzero : ¬ P 0) (hlast : P (Fin.last r))
       (hnext : ∀ i : Fin r, P i.castSucc → P i.succ) :
       ∃ t : Fin r, ∀ i : Fin (r + 1), P i ↔ t.val < i.val := by
   …

2. theorem OAI.CycleClique.Construction.pathEnds_final_segment line 52
3. theorem OAI.CycleClique.Construction.spanningPath_permute_tail line 66

   Source documentation

   Permuting the clique tail while fixing its first vertex preserves the path and all of its prefix.

   theorem spanningPath_permute_tail {V : Type*} [Fintype V]
       {G : SimpleGraph V} {x : V} {W E : Finset V} {r : ℕ}
       {f : Fin (r + 1) → V} (hf : IsSpanningPath G x W f)
       (t : Fin r) (hfinal : ∀ i : Fin (r + 1), f i ∈ E ↔ t.val < i.val)
       (hclique : G.IsClique (E : Set V)) (σ : Equiv.Perm (Fin (r + 1)))
       (hfix : ∀ i : Fin (r + 1), i.val ≤ t.val + 1 → σ i = i) :
       IsSpanningPath G x W (f ∘ σ) := by
   …

   Mentions: OAI.CycleClique.Construction.IsSpanningPath

4. theorem OAI.CycleClique.Construction.spanningPath_swap_tail line 109

   Source documentation

   Any tail vertex other than the first can be made last while the prefix and the first tail vertex stay fixed.

   theorem spanningPath_swap_tail {V : Type*} [Fintype V]
       {G : SimpleGraph V} {x : V} {W E : Finset V} {r : ℕ}
       {f : Fin (r + 1) → V} (hf : IsSpanningPath G x W f)
       (t : Fin r) (hfinal : ∀ i : Fin (r + 1), f i ∈ E ↔ t.val < i.val)
       (hclique : G.IsClique (E : Set V)) (i : Fin (r + 1))
       (hi : t.val + 1 < i.val) :
       ∃ g : Fin (r + 1) → V, IsSpanningPath G x W g ∧
         g (Fin.last r) = f i ∧
         ∀ j : Fin (r + 1), j.val ≤ t.val + 1 → g j = f j := by
   …

   Mentions: OAI.CycleClique.Construction.IsSpanningPath

5. theorem OAI.CycleClique.Construction.partial_endpoint_attachment line 136

   Source documentation

   Every endpoint except the first vertex of the fixed clique tail has no neighbour in the preceding prefix except its attachment vertex.

   theorem partial_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) :
       ∀ w ∈ pathEnds G x W r, w ≠ f t.succ →
         ∀ 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