Commit 2023-01-16 11:54 fa90299f

View on Github →

feat: port Data.Finset.Image (#1586)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/Image.lean

added theorem Disjoint.of_image_finset

added theorem Equiv.finsetCongr_apply

added theorem Equiv.finsetCongr_refl

added theorem Equiv.finsetCongr_symm

added theorem Equiv.finsetCongr_toEmbedding

added theorem Equiv.finsetCongr_trans

added theorem Finset.Nonempty.image_iff

added theorem Finset.apply_coe_mem_map

added theorem Finset.attach_image_val

added theorem Finset.attach_insert

added theorem Finset.attach_map_val

added theorem Finset.bunionᵢ_image

added theorem Finset.bunionᵢ_singleton

added theorem Finset.coe_image

added theorem Finset.coe_image_subset_range

added theorem Finset.coe_map

added theorem Finset.coe_map_subset_range

added theorem Finset.disjUnionᵢ_map

added theorem Finset.disjoint_image

added theorem Finset.disjoint_map

added theorem Finset.disjoint_range_addLeftEmbedding

added theorem Finset.disjoint_range_addRightEmbedding

added theorem Finset.erase_image_subset_image_erase

added theorem Finset.fiber_nonempty_iff_mem_image

added theorem Finset.filter_map

added theorem Finset.filter_mem_image_eq_image

added theorem Finset.fin_map

added theorem Finset.fin_mono

added theorem Finset.forall_image

added theorem Finset.forall_mem_map

added def Finset.image

added theorem Finset.image_bunionᵢ

added theorem Finset.image_bunionᵢ_filter_eq

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_inter_of_injOn

added theorem Finset.image_inter_subset

added theorem Finset.image_mono

added theorem Finset.image_singleton

added theorem Finset.image_subset_iff

added theorem Finset.image_subset_image

added theorem Finset.image_subset_image_iff

added theorem Finset.image_toFinset

added theorem Finset.image_union

added theorem Finset.image_val

added theorem Finset.image_val_of_injOn

added def Finset.map

added def Finset.mapEmbedding

added theorem Finset.mapEmbedding_apply

added theorem Finset.map_cast_heq

added theorem Finset.map_comm

added theorem Finset.map_cons

added theorem Finset.map_disjUnion'

added theorem Finset.map_disjUnion

added theorem Finset.map_disjUnionᵢ

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_subtype_subset

added theorem Finset.map_toFinset

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_image_const_self

added theorem Finset.mem_image_of_mem

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_range_iff_mem_finset_range_of_mod_eq'

added theorem Finset.mem_range_iff_mem_finset_range_of_mod_eq

added theorem Finset.mem_subtype

added theorem Finset.not_mem_map_subtype_of_not_property

added theorem Finset.property_of_mem_map_subtype

added theorem Finset.range_add

added theorem Finset.range_add_one'

added theorem Finset.range_sdiff_zero

added theorem Finset.subset_image_iff

added theorem Finset.subtype_eq_empty

added theorem Finset.subtype_map

added theorem Finset.subtype_map_of_mem

added theorem Finset.subtype_mono

added theorem Function.Commute.finset_image

added theorem Function.Commute.finset_map

added theorem Function.Injective.mem_finset_image

added theorem Function.Semiconj.finset_image

added theorem Function.Semiconj.finset_map

added theorem Multiset.toFinset_map

Modified Mathlib/Data/Int/Basic.lean