tails_append — Mathlib

English

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

Русский

Хвосты (s ++ t) равны (s.tails.map (λ l, l ++ t)) ++ t.tails.tail.

LaTeX

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

Lean4

@[simp]
theorem tails_append : ∀ s t : List α, tails (s ++ t) = (s.tails.map fun l => l ++ t) ++ t.tails.tail
  | [], [] => by simp
  | [], a :: t => by simp
  | a :: s, t => by
    simp [tails_append s t]
      -- the lemma names `inits_eq_tails` and `tails_eq_inits` are like `sublists_eq_sublists'`

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