English
Let f be appropriate, then length of the second component of mapAccumr₂ f x y c equals min(length x, length y).
Русский
Пусть f корректна, тогда длина второго компонента pair mapAccumr₂ f x y c равна min(длины x, длины y).
LaTeX
$$$$\operatorname{length}(\text{mapAccumr₂}(f,x,y,c).2) = \min(\operatorname{length}(x),\operatorname{length}(y))$$$$
Lean4
/-- Length of a list obtained using `mapAccumr₂`. -/
@[simp]
theorem length_mapAccumr₂ : ∀ (f : α → β → γ → γ × δ) (x y c), length (mapAccumr₂ f x y c).2 = min (length x) (length y)
| f, _ :: x, _ :: y, c =>
calc
succ (length (mapAccumr₂ f x y c).2) = succ (min (length x) (length y)) :=
congr_arg succ (length_mapAccumr₂ f x y c)
_ = min (succ (length x)) (succ (length y)) := Eq.symm (succ_min_succ (length x) (length y))
| _, _ :: _, [], _ => rfl
| _, [], _ :: _, _ => rfl
| _, [], [], _ => rfl
