Theorems · Theorem · combinatorics

SzemerediRegularity.card_chunk

∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U : Finset α} {hU : U ∈ P.parts},
  Fintype.card α / SzemerediRegularity.stepBound P.parts.card ≠ 0 →
    (SzemerediRegularity.chunk hP G ε hU).parts.card = 4 ^ P.parts.card

Defined in

Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqDecidableRel