factors — Mathlib

English

The product over a list of locally constant maps, evaluated at x, equals the product of the evaluations of each map on x.

Русский

Произведение по списку локально константных отображений в точке x равно произведению значений каждого отображения на x.

LaTeX

$$$\\forall (C) (x) (l : List (LocallyConstant C ℤ)), l.prod x = (l.map (LocallyConstant.evalMonoidHom x)).prod$$$

Lean4

/-- A certain explicit list of locally constant maps. The theorem `factors_prod_eq_basis` shows that the
product of the elements in this list is the delta function `spanFinBasis C s x`.
-/
def factors (x : π C (· ∈ s)) : List (LocallyConstant (π C (· ∈ s)) ℤ) :=
  List.map (fun i ↦ if x.val i = true then e (π C (· ∈ s)) i else (1 - (e (π C (· ∈ s)) i))) (s.sort (· ≥ ·))

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