biUnion_star_subset_nonuniformWitness

English

If two equipartitions P and P1 are equivalent, then SzemerediRegularity.star with P equals SzemerediRegularity.star with P1 under compatible graphs and ε values.

Русский

Если разбиения P и P1 эквиваленtны, то звёздная конструкция совпадает для обоих разбиений при совместимых графах и ε.

LaTeX

$$SzemerediRegularity.star hP G ε hU V = SzemerediRegularity.star hP' G' ε' hU' V' (при равенстве входных данных)$$

Lean4

theorem biUnion_star_subset_nonuniformWitness : (star hP G ε hU V).biUnion id ⊆ G.nonuniformWitness ε U V :=
  biUnion_subset_iff_forall_subset.2 fun _ hA => (mem_filter.1 hA).2

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