mathlib
bc3ed51b - chore(data/set/finite): use dot notation (#3151)

Commit
5 years ago
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`.
Author
Parents
Loading