Commit 2022-12-14 04:57 5b9f3b98

View on Github →

chore: restore set image notation (#1000)

depends on: #999

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Image.lean

modified theorem Function.Injective.compl_image_eq

modified theorem Function.Injective.preimage_image

modified theorem Function.LeftInverse.image_image

modified theorem Function.Surjective.image_preimage

modified theorem Set.Nonempty.image

modified theorem Set.Nonempty.image_const

modified theorem Set.Nonempty.of_image

modified theorem Set.Subsingleton.image

modified theorem Set.compl_image_set_of

modified theorem Set.eq_preimage_iff_image_eq

modified def Set.imageFactorization

modified theorem Set.image_comp

modified theorem Set.image_compl_eq

modified theorem Set.image_compl_preimage

modified theorem Set.image_compl_subset

modified theorem Set.image_congr'

modified theorem Set.image_congr

modified theorem Set.image_diff

modified theorem Set.image_diff_preimage

modified theorem Set.image_empty

modified theorem Set.image_eq_empty

modified theorem Set.image_eq_image

modified theorem Set.image_eq_range

modified theorem Set.image_eta

modified theorem Set.image_id'

modified theorem Set.image_id

modified theorem Set.image_image

modified theorem Set.image_insert_eq

modified theorem Set.image_inter

modified theorem Set.image_inter_subset

modified theorem Set.image_pair

modified theorem Set.image_perm

modified theorem Set.image_preimage_eq

modified theorem Set.image_preimage_eq_iff

modified theorem Set.image_preimage_eq_inter_range

modified theorem Set.image_preimage_subset

modified theorem Set.image_singleton

modified theorem Set.image_subset

modified theorem Set.image_subset_iff

modified theorem Set.image_subset_image_iff

modified theorem Set.image_subset_range

modified theorem Set.image_symm_diff

modified theorem Set.image_union

modified theorem Set.image_union_image_compl_eq_range

modified theorem Set.image_univ

modified theorem Set.image_univ_of_surjective

modified theorem Set.insert_image_compl_eq_range

modified theorem Set.mem_image

modified theorem Set.mem_image_elim_on

modified theorem Set.mem_image_of_mem

modified theorem Set.mem_range_of_mem_image

modified theorem Set.nonempty_image_iff

modified theorem Set.nontrivial_of_image

modified theorem Set.preimage_eq_iff_eq_image

modified theorem Set.preimage_image_eq

modified theorem Set.preimage_image_preimage

modified theorem Set.preimage_inl_image_inr

modified theorem Set.preimage_inr_image_inl

modified theorem Set.range_comp

modified theorem Set.range_diff_image

modified theorem Set.range_diff_image_subset

modified theorem Set.subset_image_compl

modified theorem Set.subset_image_diff

modified theorem Set.subset_image_symm_diff

modified theorem Set.subset_image_union

modified theorem Set.subset_preimage_image

modified theorem Set.subset_range_iff_exists_image_eq

modified theorem Subtype.coe_image_subset

modified theorem Subtype.coe_image_univ

modified theorem Subtype.image_preimage_val

Modified Mathlib/Data/Set/NAry.lean

modified theorem Set.image2_singleton_left

modified theorem Set.image2_singleton_right

modified theorem Set.image_subset_image2_left

modified theorem Set.image_subset_image2_right

Modified Mathlib/Data/Set/Sigma.lean

modified theorem Set.fst_image_sigma

modified theorem Set.fst_image_sigma_subset

modified theorem Set.image_sigmaMk_subset_sigma_right

modified theorem Set.insert_sigma

modified theorem Set.singleton_sigma

Modified Mathlib/Order/Directed.lean