iterToSum_C_X — Mathlib

English

For any c in S2, sumToIter maps the indeterminate X (Sum.inr c) to the constant C(X c).

Русский

Для любого c∈S2 отображение sumToIter переводит X(Sum.inr c) в константный C(X c).

LaTeX

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

Lean4

@[simp]
theorem iterToSum_C_X (c : S₂) : iterToSum R S₁ S₂ (C (X c)) = X (Sum.inr c) :=
  Eq.trans (eval₂_C _ _ (X c)) (eval₂_X _ _ _)

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