Theorems · Theorem · combinatorics

SimpleGraph.IsFiveWheelLike.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ

∀ {α : Type u_1} {G : SimpleGraph α} {r k : ℕ} {v w₁ w₂ : α} {s t : Finset α} [inst : DecidableEq α],
  G.IsFiveWheelLike r k v w₁ w₂ s t →
    G.CliqueFree (r + 2) →
      ∀ [inst_1 : DecidableRel G.Adj] [inst_2 : Fintype α],
        G.FiveWheelLikeFree r (k + 1) → G.minDegree ≤ (2 * r + k) * Fintype.card α / (2 * r + k + 3)

If G is a Kᵣ₊₂-free graph with n vertices containing a Wᵣ,ₖ but no Wᵣ,ₖ₊₁ then G.minDegree ≤ (2 * r + k) * n / (2 * r + k + 3)

Defined in

Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Cited by

1 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqDecidableRelFintype