law any_map_sym

bend-mathlib@0.8.1.0 · list.bend:2800

import Base

2800# Any over a map checks the composed predicate: any p (map f xs) = any (p . f) xs, reversed to rewrite toward the simple side.
2801law any_map_sym:
2802  for ~A: Type
2803  for ~B: Type
2804  for ~f: A -> B
2805  for ~p: B -> Bool
2806  for xs: List<A>
2807  {List.any(~&1, ~A, ~(x => p(f(x))), xs) == List.any(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) : Bool}