tails_eq_inits

Mathlib.Data.List.Infix

URI: https://scilib.ai/kg/mathlib#List.tails_eq_inits

← MathLib Explorer

English

Similarly, tails(l) = reverse (map reverse (inits (reverse l))).

Русский

Аналогично, tails(l) = reverse (map reverse (inits (reverse l))).

LaTeX

$$$\forall l : \text{List}(\alpha),\; l.tails = (\text{reverse} \circ \text{map} \circ \text{reverse})(\text{inits} (\text{reverse} \; l)).$$$

Lean4

theorem tails_eq_inits : ∀ l : List α, l.tails = (reverse <| map reverse <| inits <| reverse l)
  | [] => by simp
  | a :: l => by simp [tails_eq_inits l]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru