Theorems · Theorem · combinatorics

SzemerediRegularity.increment_isEquipartition

∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} (hP : P.IsEquipartition)
  (G : SimpleGraph α) [inst_2 : DecidableRel G.Adj] (ε : ℝ), (SzemerediRegularity.increment hP G ε).IsEquipartition

Defined in

Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqDecidableRel