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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A connected graph of minimum degree s has a path of order at least min(|V|,2s+1).

  1. theorem OAI.CycleClique.Construction.last_degree_index_bound line 9
  2. theorem OAI.CycleClique.Construction.first_degree_index_bound line 35
  3. theorem OAI.CycleClique.Construction.connected_long_path line 61

    Source documentation

    Manuscript Lemma clq:long-path, in the application-sized form.

    theorem connected_long_path {V : Type*} [Fintype V] {G : SimpleGraph V} {s k : ℕ}
    (hconn : G.Connected) (hdegree : ∀ v, s ≤ (G.neighborSet v).ncard)
    (hk : k ≤ 2 * s + 1) (hcard : k ≤ Fintype.card V) :
    ∃ r, ∃ f : Fin (r + 1) → V, IsIndexedPath G f ∧ k ≤ r + 1 := by
…

    Mentions: OAI.CycleClique.Construction.IsIndexedPath