isChain_destutter

Mathlib.Data.List.Destutter

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

English

For any l and R, (l.destutter R).IsChain R.

Русский

Для любого l и R, (l.destutter R).IsChain R.

LaTeX

$$$$(l.destutter R).IsChain R.$$$$

Lean4

theorem isChain_destutter : ∀ l : List α, (l.destutter R).IsChain R
  | [] => .nil
  | h :: l => l.isChain_destutter' R h

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

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

Разделы

Аффилиация

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