tail_scanr

Mathlib.Data.List.Scan

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

← MathLib Explorer

English

If 0 < length(l), then (scanr f b l).tail = scanr f b l.tail.

Русский

Если 0 < длина(l), то (scanr f b l).tail = scanr f b l.tail.

LaTeX

$$$$\forall l:\mathrm{List}(\alpha),\ 0 < \operatorname{length}(l) \Rightarrow (\operatorname{scanr} f b l).tail = (\operatorname{scanr} f b l.tail).$$$$

Lean4

theorem tail_scanr (h : 0 < l.length) : (scanr f b l).tail = scanr f b l.tail := by induction l <;> simp_all

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

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

Разделы

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

Аффилиация

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