scanl_iff_nil

Mathlib.Data.List.Scan

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

English

Scanl f b l equals the singleton [c] if and only if c = b and l is empty.

Русский

Scanl f b l равно синглетону [c] тогда и только тогда, когда c = b и l пуст.

LaTeX

$$$$\operatorname{scanl} f b l = [c] \iff c = b \wedge l = \emptyset.$$$$

Lean4

@[simp]
theorem scanl_iff_nil (c : β) : scanl f b l = [c] ↔ c = b ∧ l = [] := by constructor <;> cases l <;> simp_all

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

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

Разделы

Аффилиация

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