foldr_op_eq — Mathlib

English

If l1 ~ l2, foldr with a given associative-commutative operation op preserves the equality: foldr op a l1 = foldr op a l2.

Русский

Если l1 перестановочно эквивалентен l2, свёртка справа foldr op a по l1 равна свёртке по l2 для ассоциативной и коммутативной op.

LaTeX

$$$l_1 \\sim l_2 \\Rightarrow \\operatorname{foldr} \\operatorname{op} a\\ l_1 = \\operatorname{foldr} \\operatorname{op} a\\ l_2$$$

Lean4

theorem foldr_op_eq {l₁ l₂ : List α} {a : α} (h : l₁ ~ l₂) : l₁.foldr op a = l₂.foldr op a :=
  h.foldr_eq _

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