Commit 2023-01-21 16:19 8191b1c1

View on Github →

feat: port Data.Finset.Preimage (#1746)

Estimated changes

Modified Mathlib.lean

Created Mathlib/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.preimage_compl

added theorem Finset.preimage_empty

added theorem Finset.preimage_inter

added theorem Finset.preimage_subset

added theorem Finset.preimage_union

added theorem Finset.preimage_univ

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

added theorem Finset.subset_map_iff

Modified Mathlib/Data/Set/Finite.lean

added theorem Finset.finite_toSet

added theorem Finset.finite_toSet_toFinset

deleted theorem Finset.finite_to_set

deleted theorem Finset.finite_to_set_toFinset

added theorem List.finite_toSet

deleted theorem List.finite_to_set

added theorem Multiset.finite_toSet

added theorem Multiset.finite_toSet_toFinset

deleted theorem Multiset.finite_to_set

deleted theorem Multiset.finite_to_set_toFinset