length_mapAccumr — Mathlib

English

For all f, x, s, the length of the collected list in mapAccumr f x s equals the length of x: length((mapAccumr f x s).2) = length(x).

Русский

Для всех f, x, s длина списка, получаемого mapAccumr f x s во второй компоненте, равна длине x: |(mapAccumr f x s).snd| = |x|.

LaTeX

$$$$\operatorname{length}(\text{mapAccumr}(f,x,s).2) = \operatorname{length}(x)$$$$

Lean4

/-- Length of the list obtained by `mapAccumr`. -/
@[simp]
theorem length_mapAccumr : ∀ (f : α → γ → γ × β) (x : List α) (s : γ), length (mapAccumr f x s).2 = length x
  | f, _ :: x, s => congr_arg succ (length_mapAccumr f x s)
  | _, [], _ => rfl

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