fold_nil — Mathlib

English

Let α, β be types and f : β → α → β. For any init ∈ β, the fold of the empty sequence with init and f equals the singleton sequence consisting of init.

Русский

Пусть α, β — множества типов, f : β → α → β. Для любого начального значения init ∈ β свёртка пустой последовательности по f с начальным значением равна единичной последовательности, содержащей init.

LaTeX

$$$nil.fold\ init\ f = cons\ init\ nil$$$

Lean4

@[simp]
theorem fold_nil (init : β) (f : β → α → β) : nil.fold init f = cons init nil :=
  by
  unfold fold
  simp [corec_nil]

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