listEquivDList — Mathlib

English

There is a natural equivalence between lists and difference lists given by ofList and toList.

Русский

Существует естественное равенство между списками и списками различий, заданное через ofList и toList.

LaTeX

$$$\\text{listEquivDList} : \\text{List }\\alpha \\simeq \\text{ Batteries.DList }\\alpha$$$

Lean4

/-- The natural equivalence between lists and difference lists, using
`DList.ofList` and `DList.toList`. -/
def listEquivDList : List α ≃ DList α where
  toFun := DList.ofList
  invFun := DList.toList
  left_inv _ := DList.toList_ofList _
  right_inv _ := DList.ofList_toList _

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