scanr_iff_nil

Mathlib.Data.List.Scan

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

English

For any c, scanr f b l = [c] iff c = b and l = [].

Русский

Для любого c: scanr f b l = [c] тогда и только тогда, когда c = b и l = [].

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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