Theorems · Theorem · combinatorics

szemeredi_regularity

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (G : SimpleGraph α) [inst_2 : DecidableRel G.Adj] {ε : ℝ}
  {l : ℕ},
  0 < ε →
    l ≤ Fintype.card α →
      ∃ P, P.IsEquipartition ∧ l ≤ P.parts.card ∧ P.parts.card ≤ SzemerediRegularity.bound ε l ∧ P.IsUniform G ε

Effective Szemerédi Regularity Lemma: For any sufficiently large graph, there is an ε-uniform equipartition of bounded size (where the bound does not depend on the graph).

Defined in

Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeDecidableRel