sumToIter_Xl — Mathlib

English

Let R be a commutative semiring and S1, S2 be types. The map sumToIter sends the multivariate indeterminate X on the left component (Sum.inl b) to the indeterminate X on the left component: sumToIter(R, S1, S2)(X(Sum.inl b)) = X b for every b ∈ S1.

Русский

Пусть R — коммутативная полулекирa, S1, S2 — множества. Отображение sumToIter переводит переменную X, лежащую в левой части разложения, в соответствующую переменную X: sumToIter(R, S1, S2)(X(Sum.inl b)) = X b для любого b∈S1.

LaTeX

$$$\operatorname{sumToIter} \;R\;S_1\;S_2\bigl(X(\mathrm{Sum.inl}\, b)\bigr) = X b$$$

Lean4

@[simp]
theorem sumToIter_Xl (b : S₁) : sumToIter R S₁ S₂ (X (Sum.inl b)) = X b :=
  eval₂_X _ _ (Sum.inl b)

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