fold_cons — Mathlib

English

Let α, β be types. For any init ∈ β, f : β → α → β, a element x ∈ α and s ∈ Seq α, the fold of cons x s equals cons init (s.fold (f init x) f).

Русский

Пусть α, β — типы. Для любого init ∈ β, f : β → α → β, элемента x ∈ α и последовательности s ∈ Seq α, свёртка cons x s равна cons init (s.fold (f init x) f).

LaTeX

$$$(cons\ x\ s).fold\ init\ f = cons\ init\ (s.fold\ (f\ init\ x)\ f)$$$

Lean4

@[simp]
theorem fold_cons (init : β) (f : β → α → β) (x : α) (s : Seq α) :
    (cons x s).fold init f = cons init (s.fold (f init x) f) :=
  by
  unfold fold
  dsimp only
  congr
  rw [corec_cons]
  simp

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