reduce_append_reduce_reduce — Mathlib

English

Reducing the concatenation of two reduced lists is the same as reducing the concatenation of the original lists: reduce (reduce L1 ++ reduce L2) = reduce (L1 ++ L2).

Русский

Редукция конкатенации двух редуцированных списков равна редукции конкатенации исходных списков.

LaTeX

$$$\forall L_1,L_2 : List(Prod\;\alpha\;Bool) ,\; \mathrm{reduce}(\mathrm{reduce}(L_1) ++ \mathrm{reduce}(L_2)) = \mathrm{reduce}(L_1 ++ L_2)$$$

Lean4

@[to_additive]
theorem reduce_append_reduce_reduce : reduce (reduce L₁ ++ reduce L₂) = reduce (L₁ ++ L₂) := by
  rw [← toWord_mk (L₁ := L₁ ++ L₂), ← mul_mk, toWord_mul, toWord_mk, toWord_mk]

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