destutter'_cons_pos

Mathlib.Data.List.Destutter

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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