destutter'_cons_neg

Mathlib.Data.List.Destutter

URI: https://scilib.ai/kg/mathlib#List.destutter'_cons_neg

English

If not R b a, then (a :: l).destutter' R b = l.destutter' R b.

Русский

Если не выполняется R b a, то (a :: l).destutter' R b = l.destutter' R b.

LaTeX

$$$$\text{If } \neg R\,b\,a,\quad (a::l)\text{.destutter'}\,R\,b = l\text{.destutter'}\,R\,b.$$$$

Lean4

@[simp]
theorem destutter'_cons_neg (h : ¬R b a) : (a :: l).destutter' R b = l.destutter' R b := by rw [destutter', if_neg h]

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

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

Разделы

Аффилиация

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