Commit 2020-06-23 17:57 bc3ed51b

chore(data/set/finite): use dot notation (#3151) Rename:

• finite_insert to finite.insert;
• finite_union to finite.union;
• finite_subset to finite.subset;
• finite_image to finite.image;
• finite_dependent_image to finite.dependent_image;
• finite_map to finite.map;
• finite_image_iff_on to finite_image_iff;
• finite_preimage to finite.preimage;
• finite_sUnion to finite.sUnion;
• finite_bUnion to finite.bUnion, merge with finite_bUnion' and use f : Π i ∈ s, set α instead of f : ι → set α;
• finite_prod to finite.prod;
• finite_seq to finite.seq;
• finite_subsets_of_finite to finite.finite_subsets;
• bdd_above_finite to finite.bdd_above;
• bdd_above_finite_union to finite.bdd_above_bUnion;
• bdd_below_finite to finite.bdd_below;
• bdd_below_finite_union to finite.bdd_below_bUnion. Delete
• finite_of_finite_image_on, was a copy of finite_of_fintie_image;
• finite_bUnion': merge with finite_bUnion into finite.bUnion.