law map_take_sym

bend-mathlib@0.8.1.0 · list.bend:2623

import Base

2623# Mapping commutes with taking: map f (take n xs) = take n (map f xs), reversed to rewrite toward the simple side.
2624law map_take_sym:
2625  for ~A: Type
2626  for ~B: Type
2627  for ~f: A -> B
2628  for xs: List<A>
2629  for n: Nat
2630  {List.take(&1, B, List.map(~A, ~B, ~f, xs), n) == List.map(~A, ~B, ~f, List.take(&1, A, xs, n)) : List<B>}