law map_take

bend-mathlib@0.8.1.0 · list.bend:1184

import Base

1184# Mapping commutes with taking: map f (take n xs) = take n (map f xs).
1185law map_take:
1186  for ~A: Type
1187  for ~B: Type
1188  for ~f: A -> B
1189  for xs: List<A>
1190  for n: Nat
1191  {List.map(~A, ~B, ~f, List.take(&1, A, xs, n)) == List.take(&1, B, List.map(~A, ~B, ~f, xs), n) : List<B>}