isChain_cons_destutter'_of_rel

Mathlib.Data.List.Destutter

URI: https://scilib.ai/kg/mathlib#List.isChain_cons_destutter'_of_rel

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$$R\ a\ b \Rightarrow (a :: l.destutter'\,R\,b).IsChain\,R.$$$$

Lean4

theorem isChain_cons_destutter'_of_rel (l : List α) {a b} (hab : R a b) : (a :: l.destutter' R b).IsChain R := by
  simpa [destutter'_cons, hab] using isChain_destutter' R (b :: l) a

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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