nonuniformWitnesses — Mathlib

English

There is a finite set of witnesses of non-uniformity among the parts, obtained by mapping parts via a witnessing relation from G.

Русский

Существует конечное множество свидетелей неоднородности между частями, получаемое образом отображения через соответствие свидетельств из G.

LaTeX

$$nonuniformWitnesses G ε s = {t ∈ P.parts | s ≠ t ∧ ¬G.IsUniform ε s t}.image (G.nonuniformWitness ε s)$$

Lean4

/-- A choice of witnesses of non-uniformity among the parts of a finpartition. -/
noncomputable def nonuniformWitnesses : Finset (Finset α) :=
  {t ∈ P.parts | s ≠ t ∧ ¬G.IsUniform ε s t}.image (G.nonuniformWitness ε s)

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