Commit 2020-09-24 06:54 5e934cd9

View on Github →

chore(*): cleanup imports, split off data/finset/preimage from data/set/finite (#4221) Mostly this consists of moving some content from data.set.finite to data.finset.preimage, in order to reduce imports in data.set.finite.

Estimated changes

Modified src/category_theory/concrete_category/bundled_hom.lean

Modified src/data/finset/default.lean

Created src/data/finset/preimage.lean

added theorem finset.coe_preimage

added theorem finset.image_preimage

added theorem finset.image_preimage_of_bij

added theorem finset.image_subset_iff_subset_preimage

added theorem finset.map_subset_iff_subset_preimage

added theorem finset.mem_preimage

added theorem finset.monotone_preimage

added theorem finset.prod_preimage'

added theorem finset.prod_preimage

added theorem finset.prod_preimage_of_bij

added theorem finset.sigma_image_fst_preimage_mk

added theorem finset.sigma_preimage_mk

added theorem finset.sigma_preimage_mk_of_subset

Modified src/data/finsupp/basic.lean

Modified src/data/set/finite.lean

deleted theorem finset.coe_preimage

deleted theorem finset.image_preimage

deleted theorem finset.image_preimage_of_bij

deleted theorem finset.image_subset_iff_subset_preimage

deleted theorem finset.map_subset_iff_subset_preimage

deleted theorem finset.mem_preimage

deleted theorem finset.monotone_preimage

deleted theorem finset.prod_preimage'

deleted theorem finset.prod_preimage

deleted theorem finset.prod_preimage_of_bij

deleted theorem finset.sigma_image_fst_preimage_mk

deleted theorem finset.sigma_preimage_mk

deleted theorem finset.sigma_preimage_mk_of_subset

Modified src/order/filter/at_top_bot.lean

Modified src/topology/bases.lean