aeval_comp_bind₁ — Mathlib

English

Composition of a evaluation map with bind₁ equals evaluation with the composed inner evaluations.

Русский

Сложение отображения вычисления с bind₁ дает вычисление с соответствующими вложенными вычислениями.

LaTeX

$$$$ (\mathrm{aeval}\, f) \circ (\mathrm{bind}_1\, g) = \mathrm{aeval}\, (\lambda i. \mathrm{aeval}\, f\; (g i)) $$$$

Lean4

theorem aeval_comp_bind₁ [Algebra R S] (f : τ → S) (g : σ → MvPolynomial τ R) :
    (aeval f).comp (bind₁ g) = aeval fun i => aeval f (g i) :=
  by
  ext1
  apply aeval_bind₁

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