inits_append — Mathlib

English

For any s,t, inits(s ++ t) = s.inits ++ t.inits.tail.map (λ l, s ++ l).

Русский

Для любых s,t: инициалы (s ++ t) равны s.inits ++ (t.inits.tail) с добавлением s в начало каждого l.

LaTeX

$$$\forall s,t : \text{List}(\alpha),\; \text{inits}(s ++ t) = s.\text{inits} ++ t.\text{inits}.tail.map (\lambda l. s ++ l).$$$

Lean4

@[simp]
theorem inits_append : ∀ s t : List α, inits (s ++ t) = s.inits ++ t.inits.tail.map fun l => s ++ l
  | [], [] => by simp
  | [], a :: t => by simp
  | a :: s, t => by simp [inits_append s t, Function.comp_def]

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