recOfList

Mathlib.SetTheory.Lists

URI: https://scilib.ai/kg/mathlib#Lists'.recOfList

Lean4

/-- Recursion/induction principle for `Lists'.ofList`. -/
@[elab_as_elim]
def recOfList {motive : Lists' α true → Sort*} (ofList : ∀ l, motive (ofList l)) : ∀ l, motive l := fun l ↦
  cast (by simp) <| ofList (l.toList)

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

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

Разделы

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

Аффилиация

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