scanr_append — Mathlib

English

For lists l1 and l2, scanr f b (l1 ++ l2) equals scanr f (foldr f b l2) l1 concatenated with the tail of scanr f b l2.

Русский

Для списков l1 и l2 выполняется: scanr f b (l1 ++ l2) = scanr f (foldr f b l2) l1 ++ (scanr f b l2).tail.

LaTeX

$$$$\operatorname{scanr} f b (l_1 \;\;\mathrm{++}\;\; l_2) = \operatorname{scanr} f (\operatorname{foldr} f b l_2) l_1 \;\; \mathrm{++} \;\; (\operatorname{scanr} f b l_2).\mathrm{tail}.$$$$

Lean4

theorem scanr_append (l₁ l₂ : List α) : scanr f b (l₁ ++ l₂) = (scanr f (foldr f b l₂) l₁) ++ (scanr f b l₂).tail := by
  induction l₁ <;> induction l₂ <;> simp [*]

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