destutter_eq_self_iff

Mathlib.Data.List.Destutter

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

English

destutter_eq_self_iff: l.destutter R = l ↔ l.IsChain R.

Русский

destutter_eq_self_iff: l.destutter R = l ⇔ l.IsChain R.

LaTeX

$$$$l.destutter R = l \iff l.IsChain R.$$$$

Lean4

@[simp]
theorem destutter_eq_self_iff : ∀ l : List α, l.destutter R = l ↔ l.IsChain R
  | [] => by simp
  | a :: l => l.destutter'_eq_self_iff R a

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

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

Разделы

Аффилиация

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