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

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The full prescribed-length coloured-path lemma of manuscript Section 3.

  1. def OAI.CycleClique.Construction.indexedSupport line 11
  2. theorem OAI.CycleClique.Construction.mem_indexedSupport line 16
  3. theorem OAI.CycleClique.Construction.indexedSupport_range line 21
  4. theorem OAI.CycleClique.Construction.indexedSupport_card line 26
  5. theorem OAI.CycleClique.Construction.colored_path_prescribed_length line 32

    Source documentation

    Prescribed-length paths with differently coloured endpoints.

    theorem colored_path_prescribed_length {V : Type*} [Fintype V] [DecidableEq V]
    {H : SimpleGraph V} {s : ℕ} (hs : 4 ≤ s)
    (hconn : H.Connected) (hnonbip : ¬ H.IsBipartite) (hno : H.cliqueNum < s)
    (hdegree : ∀ v, s ≤ (H.neighborSet v).ncard)
    (hpair : ∀ a b, a ≠ b → ¬ H.Adj a b →
      2 * s ≤ (closedNeighborhood H {a, b}).card)
    (χ : V → Fin 2) (hnonconstant : ∃ a b, χ a ≠ χ b)
    {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (hℓmax : ℓ ≤ 2 * s - 2) :
    ∃ g : Fin (ℓ + 1) → V, IsIndexedPath H g ∧ χ (g 0) ≠ χ (g (Fin.last ℓ)) := by
…

    Mentions: OAI.CycleClique.Construction.closedNeighborhood, OAI.CycleClique.Construction.IsIndexedPath