foldl_op_eq_op_foldr_assoc — Mathlib

English

Same principle as above, expressed with a variant naming: for associative op, for all l, a1, a2, foldl op a1 l with right element a2 equals a1 ⋆ foldr (⋆) a2 l.

Русский

Та же идея, как и выше, выраженная другим названием: для ассоциативной операции op, для любого l, a1, a2 имеем: foldl op a1 l = a1 ⋆ foldr (⋆) a2 l.

LaTeX

$$$$\forall l:\ List\ α\,\forall a_1,a_2:\alpha,\ foldl op a_1 l = a_1 \ast foldr (\lambda x y. x \ast y) a_2 l.$$$$

Lean4

theorem foldl_op_eq_op_foldr_assoc : ∀ {l : List α} {a₁ a₂}, ((l <*> a₁) ⋆ a₂) = a₁ ⋆ l.foldr (· ⋆ ·) a₂
  | [], _, _ => rfl
  | a :: l, a₁, a₂ => by simp only [foldl_cons, foldr_cons, foldl_assoc, ha.assoc]; rw [foldl_op_eq_op_foldr_assoc]

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