mathlib

7fea719c - feat(data/set/basic): Laws for n-ary image (#13011)

feat(data/set/basic): Laws for n-ary image (#13011) Prove left/right commutativity, distributivity of `set.image2` in the style of `set.image2_assoc`. Also add `forall₃_imp` and `Exists₃.imp`.