Commit 2020-07-12 03:42 b0473968

feat(data/set/finite): add a version of prod_preimage for inj_on (#3342)

• rename finset.prod_preimage to finset.prod_preimage_of_bij;
• new prod_preimage assumes ∀ x ∈ s, x ∉ range f, g x = 1;
• rename finset.image_preimage to finset.image_preimage_of_bij;
• new finset.image_preimage says image f (preimage s hf) = s.filter (λ x, x ∈ set.range f);
• change the order of implicit arguments in the definition of set.inj_on;
• add prod_filter_of_ne;
• use coe instead of subtype.val in prod_attach;
• add finset.image_subset_iff, finset.image_subset_iff_subset_preimage, finset.map_subset_iff_subset_preimage.