take_inits — Mathlib

English

For any n, taking the first n elements then the inits is the same as taking the inits of l and then taking the first n elements; more precisely (l.take n).inits = l.inits.take(n+1).

Русский

Для любого n выполняется (l.take n).inits = l.inits.take(n+1).

LaTeX

$$$(\\operatorname{take} l\\, n).\\operatorname{inits} = \\operatorname{inits} l.\\operatorname{take}(n+1)$$$

Lean4

theorem take_inits {n} : (l.take n).inits = l.inits.take (n + 1) := by
  apply ext_getElem <;> (simp [take_take] <;> omega)

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