destutter_of_isChain

Mathlib.Data.List.Destutter

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

Lean4

theorem destutter_of_isChain : ∀ l : List α, l.IsChain R → l.destutter R = l
  | [], _ => rfl
  | _ :: l, h => l.destutter'_of_isChain_cons _ h

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

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

Разделы

Аффилиация

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