Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-30 13:52 de62b061

View on Github →

chore(data/set/pointwise): Golf using set.image2 API (#13051) Add some more set.image2 API and demonstrate use by golfing all relevant data.set.pointwise declarations. Other additions

Estimated changes

modified theorem set.image2_assoc
modified theorem set.image2_left_comm
modified theorem set.image2_right_comm
added theorem set.image_comm
modified theorem set.image_image2_distrib
modified theorem set.Inter_inv
modified theorem set.Union_inv
modified theorem set.compl_inv
modified theorem set.finite.inv
modified theorem set.finite.mul
added theorem set.finite.smul
modified theorem set.finite.smul_set
modified theorem set.image_inv
modified theorem set.image_mul
added theorem set.image_op_inv
modified theorem set.image_op_mul
modified theorem set.inter_inv
modified theorem set.inv_empty
modified theorem set.inv_mem_inv
modified theorem set.inv_preimage
modified theorem set.inv_singleton
modified theorem set.inv_subset
modified theorem set.inv_subset_inv
modified theorem set.inv_univ
modified theorem set.mem_inv
modified theorem set.nonempty.inv
modified theorem set.nonempty.mul
added theorem set.nonempty.smul
added theorem set.nonempty.smul_set
added theorem set.nonempty.vsub
modified theorem set.nonempty_inv
modified theorem set.union_inv