Commit 2022-12-12 07:45 a6ba4bb2

View on Github →

feat: Port Data.Set.Image (#949) mathlib3 SHA: f178c0e25af359f6cbc72a96a243efd3b12423a3

depends on: #892

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/Image.lean

added theorem Function.Commute.set_image

added theorem Function.Injective.compl_image_eq

added theorem Function.Injective.exists_unique_of_mem_range

added theorem Function.Injective.image_injective

added theorem Function.Injective.mem_range_iff_exists_unique

added theorem Function.Injective.mem_set_image

added theorem Function.Injective.preimage_image

added theorem Function.Injective.preimage_surjective

added theorem Function.Injective.subsingleton_image_iff

added theorem Function.LeftInverse.image_image

added theorem Function.LeftInverse.preimage_preimage

added theorem Function.Semiconj.set_image

added theorem Function.Surjective.image_preimage

added theorem Function.Surjective.image_surjective

added theorem Function.Surjective.nonempty_preimage

added theorem Function.Surjective.preimage_injective

added theorem Function.Surjective.preimage_subset_preimage_iff

added theorem Function.Surjective.range_comp

added theorem Nat.mem_range_succ

added theorem Option.injective_iff

added theorem Option.range_eq

added theorem Prod.range_fst

added theorem Prod.range_snd

added theorem Set.Nonempty.image

added theorem Set.Nonempty.image_const

added theorem Set.Nonempty.of_image

added theorem Set.Nonempty.preimage'

added theorem Set.Nonempty.preimage

added theorem Set.Nontrivial.image

added theorem Set.Nontrivial.preimage

added theorem Set.Subsingleton.image

added theorem Set.Subsingleton.preimage

added theorem Set.Sum.elim_range

added theorem Set.apply_rangeSplitting

added theorem Set.ball_image_iff

added theorem Set.ball_image_of_ball

added theorem Set.bex_image_iff

added theorem Set.coe_comp_rangeFactorization

added theorem Set.comp_rangeSplitting

added theorem Set.compl_compl_image

added theorem Set.compl_image

added theorem Set.compl_image_set_of

added theorem Set.compl_range_inl

added theorem Set.compl_range_inr

added theorem Set.compl_range_some

added theorem Set.eq_preimage_iff_image_eq

added theorem Set.eq_preimage_subtype_val_iff

added theorem Set.exists_image_iff

added theorem Set.exists_range_iff'

added theorem Set.exists_range_iff

added theorem Set.exists_subset_range_and_iff

added theorem Set.exists_subset_range_iff

added theorem Set.exists_subtype_range_iff

added theorem Set.forall_range_iff

added theorem Set.forall_subtype_range_iff

added def Set.imageFactorization

added theorem Set.imageFactorization_eq

added theorem Set.image_comm

added theorem Set.image_comp

added theorem Set.image_compl_eq

added theorem Set.image_compl_preimage

added theorem Set.image_compl_subset

added theorem Set.image_congr'

added theorem Set.image_congr

added theorem Set.image_diff

added theorem Set.image_diff_preimage

added theorem Set.image_empty

added theorem Set.image_eq_empty

added theorem Set.image_eq_image

added theorem Set.image_eq_preimage_of_inverse

added theorem Set.image_eq_range

added theorem Set.image_eta

added theorem Set.image_id'

added theorem Set.image_id

added theorem Set.image_image

added theorem Set.image_injective

added theorem Set.image_insert_eq

added theorem Set.image_inter

added theorem Set.image_inter_nonempty_iff

added theorem Set.image_inter_on

added theorem Set.image_inter_preimage

added theorem Set.image_inter_subset

added theorem Set.image_pair

added theorem Set.image_perm

added theorem Set.image_preimage_eq

added theorem Set.image_preimage_eq_iff

added theorem Set.image_preimage_eq_inter_range

added theorem Set.image_preimage_eq_of_subset

added theorem Set.image_preimage_inl_union_image_preimage_inr

added theorem Set.image_preimage_inter

added theorem Set.image_preimage_subset

added theorem Set.image_singleton

added theorem Set.image_subset

added theorem Set.image_subset_iff

added theorem Set.image_subset_image_iff

added theorem Set.image_subset_preimage_of_inverse

added theorem Set.image_subset_range

added theorem Set.image_surjective

added theorem Set.image_swap_eq_preimage_swap

added theorem Set.image_symm_diff

added theorem Set.image_union

added theorem Set.image_union_image_compl_eq_range

added theorem Set.image_univ

added theorem Set.image_univ_of_surjective

added theorem Set.insert_image_compl_eq_range

added theorem Set.insert_none_range_some

added theorem Set.inter_preimage_subset

added theorem Set.isCompl_range_inl_range_inr

added theorem Set.isCompl_range_some_none

added theorem Set.leftInverse_rangeSplitting

added theorem Set.mem_compl_image

added theorem Set.mem_image

added theorem Set.mem_image_elim

added theorem Set.mem_image_elim_on

added theorem Set.mem_image_iff_bex

added theorem Set.mem_image_iff_of_inverse

added theorem Set.mem_image_of_mem

added theorem Set.mem_preimage

added theorem Set.mem_range

added theorem Set.mem_range_of_mem_image

added theorem Set.mem_range_self

added theorem Set.nonempty_image_iff

added theorem Set.nonempty_of_nonempty_preimage

added theorem Set.nontrivial_of_image

added theorem Set.nontrivial_of_preimage

added def Set.preimage

added theorem Set.preimage_comp

added theorem Set.preimage_comp_eq

added theorem Set.preimage_compl

added theorem Set.preimage_compl_eq_image_compl

added theorem Set.preimage_congr

added theorem Set.preimage_const

added theorem Set.preimage_const_of_mem

added theorem Set.preimage_const_of_not_mem

added theorem Set.preimage_diff

added theorem Set.preimage_empty

added theorem Set.preimage_eq_iff_eq_image

added theorem Set.preimage_eq_preimage'

added theorem Set.preimage_eq_preimage

added theorem Set.preimage_id'

added theorem Set.preimage_id

added theorem Set.preimage_id_eq

added theorem Set.preimage_image_eq

added theorem Set.preimage_image_preimage

added theorem Set.preimage_injective

added theorem Set.preimage_inl_image_inr

added theorem Set.preimage_inl_range_inr

added theorem Set.preimage_inr_image_inl

added theorem Set.preimage_inr_range_inl

added theorem Set.preimage_inter

added theorem Set.preimage_inter_range

added theorem Set.preimage_ite

added theorem Set.preimage_iterate_eq

added theorem Set.preimage_mono

added theorem Set.preimage_preimage

added theorem Set.preimage_range

added theorem Set.preimage_rangeSplitting

added theorem Set.preimage_range_inter

added theorem Set.preimage_set_of_eq

added theorem Set.preimage_singleton_eq_empty

added theorem Set.preimage_singleton_nonempty

added theorem Set.preimage_subset_iff

added theorem Set.preimage_subset_image_of_inverse

added theorem Set.preimage_subset_preimage_iff

added theorem Set.preimage_subtype_coe_eq_compl

added theorem Set.preimage_surjective

added theorem Set.preimage_union

added theorem Set.preimage_univ

added theorem Set.prod_quotient_preimage_eq_image

added def Set.range

added def Set.rangeFactorization

added theorem Set.rangeFactorization_coe

added theorem Set.rangeFactorization_eq

added theorem Set.rangeSplitting_injective

added theorem Set.range_comp

added theorem Set.range_comp_subset_range

added theorem Set.range_const

added theorem Set.range_const_subset

added theorem Set.range_diff_image

added theorem Set.range_diff_image_subset

added theorem Set.range_eq_empty

added theorem Set.range_eq_empty_iff

added theorem Set.range_eq_iff

added theorem Set.range_eval

added theorem Set.range_id'

added theorem Set.range_id

added theorem Set.range_iff_surjective

added theorem Set.range_image

added theorem Set.range_inclusion

added theorem Set.range_inl_inter_range_inr

added theorem Set.range_inl_union_range_inr

added theorem Set.range_inr_inter_range_inl

added theorem Set.range_inr_union_range_inl

added theorem Set.range_ite_subset'

added theorem Set.range_ite_subset

added theorem Set.range_nonempty

added theorem Set.range_nonempty_iff_nonempty

added theorem Set.range_quot_lift

added theorem Set.range_quot_mk

added theorem Set.range_quotient_lift

added theorem Set.range_quotient_lift_on'

added theorem Set.range_quotient_mk'

added theorem Set.range_quotient_mk

added theorem Set.range_some_inter_none

added theorem Set.range_some_union_none

added theorem Set.range_subset_iff

added theorem Set.range_subset_singleton

added theorem Set.range_subtype_map

added theorem Set.range_unique

added theorem Set.rightInverse_rangeSplitting

added theorem Set.subset_image_compl

added theorem Set.subset_image_diff

added theorem Set.subset_image_symm_diff

added theorem Set.subset_image_union

added theorem Set.subset_preimage_image

added theorem Set.subset_preimage_univ

added theorem Set.subset_range_iff_exists_image_eq

added theorem Set.subsingleton_of_image

added theorem Set.subsingleton_of_preimage

added theorem Set.subsingleton_range

added theorem Set.surjective_onto_image

added theorem Set.surjective_onto_range

added theorem Set.union_preimage_subset

added theorem Subtype.coe_image

added theorem Subtype.coe_image_of_subset

added theorem Subtype.coe_image_subset

added theorem Subtype.coe_image_univ

added theorem Subtype.coe_preimage_self

added theorem Subtype.exists_set_subtype

added theorem Subtype.image_preimage_coe

added theorem Subtype.image_preimage_val

added theorem Subtype.preimage_coe_compl'

added theorem Subtype.preimage_coe_compl

added theorem Subtype.preimage_coe_eq_empty

added theorem Subtype.preimage_coe_eq_preimage_coe_iff

added theorem Subtype.preimage_coe_inter_self

added theorem Subtype.preimage_coe_nonempty

added theorem Subtype.preimage_val_eq_preimage_val_iff

added theorem Subtype.range_coe

added theorem Subtype.range_coe_subtype

added theorem Subtype.range_val

added theorem Subtype.range_val_subtype

added theorem Sum.range_eq

added theorem WithBot.range_eq

added theorem WithTop.range_eq