Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-08 18:41 cabb8aee

View on Github →

refactor(data/finset/image): split out of data/finset/basic (#17852) This somewhat matches the split for data/set/basic, and makes the file shorter by a reasonable amount. The proof of bUnion_singleton_eq_self was tweaked slightly so that it didn't need to move file.

Estimated changes

deleted theorem disjoint.of_image_finset
deleted theorem equiv.finset_congr_apply
deleted theorem equiv.finset_congr_refl
deleted theorem equiv.finset_congr_symm
deleted theorem equiv.finset_congr_trans
deleted theorem finset.apply_coe_mem_map
deleted theorem finset.attach_image_coe
deleted theorem finset.attach_image_val
deleted theorem finset.attach_insert
deleted theorem finset.attach_map_val
deleted theorem finset.bUnion_image
deleted theorem finset.bUnion_singleton
deleted theorem finset.coe_image
deleted theorem finset.coe_map
deleted theorem finset.disj_Union_map
deleted theorem finset.disjoint_image
deleted theorem finset.disjoint_map
deleted theorem finset.filter_map
deleted theorem finset.fin_map
deleted theorem finset.fin_mono
deleted theorem finset.forall_mem_map
deleted def finset.image
deleted theorem finset.image_bUnion
deleted theorem finset.image_comm
deleted theorem finset.image_congr
deleted theorem finset.image_const
deleted theorem finset.image_empty
deleted theorem finset.image_eq_empty
deleted theorem finset.image_erase
deleted theorem finset.image_filter
deleted theorem finset.image_id'
deleted theorem finset.image_id
deleted theorem finset.image_image
deleted theorem finset.image_insert
deleted theorem finset.image_inter
deleted theorem finset.image_inter_subset
deleted theorem finset.image_mono
deleted theorem finset.image_singleton
deleted theorem finset.image_subset_iff
deleted theorem finset.image_subset_image
deleted theorem finset.image_to_finset
deleted theorem finset.image_union
deleted theorem finset.image_val
deleted def finset.map
deleted theorem finset.map_cast_heq
deleted theorem finset.map_comm
deleted theorem finset.map_cons
deleted theorem finset.map_disj_Union
deleted theorem finset.map_disj_union'
deleted theorem finset.map_disj_union
deleted theorem finset.map_empty
deleted theorem finset.map_eq_empty
deleted theorem finset.map_eq_image
deleted theorem finset.map_erase
deleted theorem finset.map_filter
deleted theorem finset.map_inj
deleted theorem finset.map_injective
deleted theorem finset.map_insert
deleted theorem finset.map_inter
deleted theorem finset.map_map
deleted theorem finset.map_nonempty
deleted theorem finset.map_perm
deleted theorem finset.map_refl
deleted theorem finset.map_singleton
deleted theorem finset.map_subset_map
deleted theorem finset.map_subtype_subset
deleted theorem finset.map_to_finset
deleted theorem finset.map_union
deleted theorem finset.map_val
deleted theorem finset.mem_fin
deleted theorem finset.mem_image
deleted theorem finset.mem_image_const
deleted theorem finset.mem_image_of_mem
deleted theorem finset.mem_map'
deleted theorem finset.mem_map
deleted theorem finset.mem_map_equiv
deleted theorem finset.mem_map_of_mem
deleted theorem finset.mem_subtype
deleted theorem finset.nonempty.image_iff
deleted theorem finset.range_add
deleted theorem finset.range_add_one'
deleted theorem finset.range_sdiff_zero
deleted theorem finset.subset_image_iff
deleted theorem finset.subtype_eq_empty
deleted theorem finset.subtype_map
deleted theorem finset.subtype_map_of_mem
deleted theorem finset.subtype_mono
deleted theorem multiset.to_finset_map
added theorem finset.attach_insert
added theorem finset.attach_map_val
added theorem finset.bUnion_image
added theorem finset.coe_image
added theorem finset.coe_map
added theorem finset.disj_Union_map
added theorem finset.disjoint_image
added theorem finset.disjoint_map
added theorem finset.filter_map
added theorem finset.fin_map
added theorem finset.fin_mono
added theorem finset.forall_mem_map
added def finset.image
added theorem finset.image_bUnion
added theorem finset.image_comm
added theorem finset.image_congr
added theorem finset.image_const
added theorem finset.image_empty
added theorem finset.image_eq_empty
added theorem finset.image_erase
added theorem finset.image_filter
added theorem finset.image_id'
added theorem finset.image_id
added theorem finset.image_image
added theorem finset.image_insert
added theorem finset.image_inter
added theorem finset.image_mono
added theorem finset.image_singleton
added theorem finset.image_to_finset
added theorem finset.image_union
added theorem finset.image_val
added def finset.map
added theorem finset.map_cast_heq
added theorem finset.map_comm
added theorem finset.map_cons
added theorem finset.map_disj_Union
added theorem finset.map_disj_union'
added theorem finset.map_disj_union
added theorem finset.map_empty
added theorem finset.map_eq_empty
added theorem finset.map_eq_image
added theorem finset.map_erase
added theorem finset.map_filter
added theorem finset.map_inj
added theorem finset.map_injective
added theorem finset.map_insert
added theorem finset.map_inter
added theorem finset.map_map
added theorem finset.map_nonempty
added theorem finset.map_perm
added theorem finset.map_refl
added theorem finset.map_singleton
added theorem finset.map_subset_map
added theorem finset.map_to_finset
added theorem finset.map_union
added theorem finset.map_val
added theorem finset.mem_fin
added theorem finset.mem_image
added theorem finset.mem_image_const
added theorem finset.mem_map'
added theorem finset.mem_map
added theorem finset.mem_map_equiv
added theorem finset.mem_map_of_mem
added theorem finset.mem_subtype
added theorem finset.range_add
added theorem finset.range_add_one'
added theorem finset.subtype_map
added theorem finset.subtype_mono
added theorem multiset.to_finset_map