Commit 2022-07-05 19:14 f10d0abc

feat(*): add lemmas about sigma types (#15085)

• move set.range_sigma_mk to data.set.sigma;
• add set.preimage_image_sigma_mk_of_ne, set.image_sigma_mk_preimage_sigma_map_subset, and set.image_sigma_mk_preimage_sigma_map;
• add function.injective.of_sigma_map and function.injective.sigma_map_iff;
• don't use pattern matching in the definition of prod.to_sigma;
• add filter.map_sigma_mk_comap