isList_toList

Mathlib.SetTheory.Lists

URI: https://scilib.ai/kg/mathlib#Lists.isList_toList

English

For any l, the nested-list encoded as ofList l carries a canonical list structure: isList (ofList l).

Русский

Для любого l вложенный список, закодированный как ofList l, имеет каноническую структуру списка: IsList (ofList l).

LaTeX

$$$(\\text{Lists}.toList(\\text{ofList}(l))) = l$$$

Lean4

theorem isList_toList (l : List (Lists α)) : IsList (ofList l) :=
  Eq.refl _

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

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

Разделы

Аффилиация

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