Commit 2022-03-28 23:54 7fea719c

View on Github →

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.

Estimated changes

Modified src/data/set/basic.lean

added theorem set.image2_comm

added theorem set.image2_eq_empty_iff

added theorem set.image2_left_comm

added theorem set.image2_nonempty_iff

added theorem set.image2_right_comm

added theorem set.image3_mono

added theorem set.image_image2_distrib

added theorem set.image_image2_distrib_left

added theorem set.image_image2_distrib_right

modified theorem set.nonempty.image2

Modified src/logic/basic.lean

modified theorem Exists.imp

modified theorem Exists₂.imp

added theorem Exists₃.imp

modified theorem exists₂_congr

modified theorem forall_imp

modified theorem forall₂_imp

added theorem forall₃_imp