fold_head — Mathlib

English

For any s ∈ Seq α, init ∈ β and f : β → α → β, the head of the folded sequence (s.fold init f) is init.

Русский

Для любой последовательности s ∈ Seq α, начального значения init ∈ β и функции f : β → α → β, голова свёртки s.fold init f равна init.

LaTeX

$$$\text{head}(s.fold\ init\ f) = init$$$

Lean4

@[simp]
theorem fold_head (init : β) (f : β → α → β) (s : Seq α) : (s.fold init f).head = init := by simp [fold]

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