Theorems · Definition · combinatorics

SzemerediRegularity.chunk

{α : Type u_1} →
  [inst : Fintype α] →
    [inst_1 : DecidableEq α] →
      {P : Finpartition Finset.univ} →
        P.IsEquipartition →
          (G : SimpleGraph α) → [DecidableRel G.Adj] → ℝ → {U : Finset α} → U ∈ P.parts → Finpartition U

The portion of SzemerediRegularity.increment which partitions U.

Defined in

Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Cited by

11 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqDecidableRel