star — Mathlib

English

The star construction is equal to the filter of the chunk by nonuniform witnesses: SzemerediRegularity.star hP G ε hU V equals the filter of SzemerediRegularity.chunk hP G ε hU by the predicate A ⊆ G.nonuniformWitness ε U V.

Русский

Звёздная конструкция равна фильтру chunk по подмножителю A, который подкрепляется nonuniformWitness.

LaTeX

$$SzemerediRegularity.star hP G ε hU V = Finset.filter (fun A => A ⊆ G.nonuniformWitness ε U V) (SzemerediRegularity.chunk hP G ε hU).parts$$

Lean4

/-- The portion of `SzemerediRegularity.chunk` which is contained in the witness of non-uniformity
of `U` and `V`. -/
noncomputable def star (V : Finset α) : Finset (Finset α) :=
  {A ∈ (chunk hP G ε hU).parts | A ⊆ G.nonuniformWitness ε U V}

Похожие утверждения