zipWith_toList — Mathlib

English

toList of zipWith equals List.zipWith of underlying lists: (Vector.zipWith f x y).toList = List.zipWith f x.toList y.toList.

Русский

toList у Vector.zipWith равен List.zipWith для базовых списков: (Vector.zipWith f x y).toList = List.zipWith f x.toList y.toList.

LaTeX

$$$\ (Vector.zipWith f x y).toList = List.zipWith f x.toList y.toList$$$

Lean4

@[simp]
theorem zipWith_toList (x : Vector α n) (y : Vector β n) :
    (Vector.zipWith f x y).toList = List.zipWith f x.toList y.toList :=
  rfl

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