scanr_ne_nil

Mathlib.Data.List.Scan

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

English

For all f, b, l, the scanr sequence is nonempty.

Русский

Для всех f, b, l последовательность scanr непуста.

LaTeX

$$$$\operatorname{scanr} f b l \neq \emptyset.$$$$

Lean4

@[simp]
theorem scanr_ne_nil : scanr f b l ≠ [] := by simp [scanr]

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

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

Разделы

Аффилиация

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