Theorems · Theorem · combinatorics

SimpleGraph.eventually_isContained_of_card_edgeFinset

∀ {W : Type u_1} (H : SimpleGraph W) {ε : ℝ},
  0 < ε →
    ∀ᶠ (n : ℕ) in Filter.atTop,
      ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj],
        ↑G.edgeFinset.card ≥ (H.turanDensity + ε) * ↑(n.choose 2) → H.IsContained G

Simple graphs on n vertices having at least (turanDensity H + o(1)) * n ^ 2 edges contain H, for sufficiently large n.

Defined in

Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Cited by

1 results in Mathlib

Foundations

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