isGood — Mathlib

English

The predicate isGood picks out those products whose evaluation is outside the span of earlier evaluations; i.e., they form a basis of LocallyConstant ℤ.

Русский

Утверждение isGood выбирает такие продукты, чьи значения выходят за линейную оболочку ранних значений; они образуют базис LocallyConstant ℤ.

LaTeX

$$$$ \\text{isGood}(l) := l.\\mathrm{eval}\\, C \\notin \\operatorname{span}_{\\mathbb{Z}}( \\{ \\mathrm{Products.eval}\\, C\\ y \\mid y < l\\} ).$$$$

Lean4

/-- The predicate on products which we prove picks out a basis of `LocallyConstant C ℤ`. We call such a
product "good".
-/
def isGood (l : Products I) : Prop :=
  l.eval C ∉ Submodule.span ℤ ((Products.eval C) '' {m | m < l})

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