Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-06 15:46 bcd13a77

View on Github →

refactor(data/equiv): split out ./set from ./basic (#9560) This move all the equivalences between sets-coerced-to-types to a new file, which makes equiv/basic a slightly more manageable size. The only non-move change in this PR is the rewriting of equiv.of_bijective to not go via equiv.of_injective, as we already have all the fields available directly and this allows the latter to move to a separate file. This will allow us to import order_dual.lean earlier, as we no longer have to define boolean algebras before equivalences are available. This relates to #4758.

Estimated changes

Modified src/algebra/group/ulift.lean

Modified src/data/equiv/basic.lean

deleted theorem dite_comp_equiv_update

deleted theorem equiv.apply_of_injective_symm

deleted theorem equiv.eq_image_iff_symm_image_eq

deleted theorem equiv.eq_preimage_iff_image_eq

deleted def equiv.image

deleted theorem equiv.image_eq_iff_eq

deleted theorem equiv.image_preimage

deleted theorem equiv.image_subset

deleted theorem equiv.image_symm_image

deleted theorem equiv.of_injective_symm_apply

deleted def equiv.of_left_inverse'

deleted theorem equiv.of_left_inverse'_eq_of_injective

deleted def equiv.of_left_inverse

deleted theorem equiv.of_left_inverse_eq_of_injective

deleted theorem equiv.preimage_eq_iff_eq_image

deleted theorem equiv.preimage_image

deleted theorem equiv.preimage_subset

deleted theorem equiv.preimage_symm_preimage

deleted theorem equiv.prod_assoc_preimage

deleted theorem equiv.range_eq_univ

deleted theorem equiv.self_comp_of_injective_symm

deleted theorem equiv.set.image_symm_preimage

deleted theorem equiv.set.insert_apply_left

deleted theorem equiv.set.insert_apply_right

deleted theorem equiv.set.insert_symm_apply_inl

deleted theorem equiv.set.insert_symm_apply_inr

deleted theorem equiv.set.sum_compl_apply_inl

deleted theorem equiv.set.sum_compl_apply_inr

deleted theorem equiv.set.sum_compl_symm_apply

deleted theorem equiv.set.sum_compl_symm_apply_compl

deleted theorem equiv.set.sum_compl_symm_apply_of_mem

deleted theorem equiv.set.sum_compl_symm_apply_of_not_mem

deleted theorem equiv.set.sum_diff_subset_apply_inl

deleted theorem equiv.set.sum_diff_subset_apply_inr

deleted theorem equiv.set.sum_diff_subset_symm_apply_of_mem

deleted theorem equiv.set.sum_diff_subset_symm_apply_of_not_mem

deleted theorem equiv.set.union_apply_left

deleted theorem equiv.set.union_apply_right

deleted theorem equiv.set.union_symm_apply_left

deleted theorem equiv.set.union_symm_apply_right

deleted def equiv.set_congr

deleted def equiv.set_prod_equiv_sigma

deleted theorem equiv.symm_image_image

deleted theorem equiv.symm_preimage_preimage

deleted theorem set.image_equiv_eq_preimage_symm

deleted theorem set.mem_image_equiv

deleted theorem set.preimage_equiv_eq_image_symm

Modified src/data/equiv/local_equiv.lean

Modified src/data/equiv/mul_add.lean

Created src/data/equiv/set.lean

added theorem dite_comp_equiv_update

added theorem equiv.apply_of_injective_symm

added theorem equiv.eq_image_iff_symm_image_eq

added theorem equiv.eq_preimage_iff_image_eq

added def equiv.image

added theorem equiv.image_eq_iff_eq

added theorem equiv.image_preimage

added theorem equiv.image_subset

added theorem equiv.image_symm_image

added theorem equiv.of_injective_symm_apply

added def equiv.of_left_inverse'

added theorem equiv.of_left_inverse'_eq_of_injective

added def equiv.of_left_inverse

added theorem equiv.of_left_inverse_eq_of_injective

added theorem equiv.preimage_eq_iff_eq_image

added theorem equiv.preimage_image

added theorem equiv.preimage_subset

added theorem equiv.preimage_symm_preimage

added theorem equiv.prod_assoc_preimage

added theorem equiv.range_eq_univ

added theorem equiv.self_comp_of_injective_symm

added theorem equiv.set.image_symm_preimage

added theorem equiv.set.insert_apply_left

added theorem equiv.set.insert_apply_right

added theorem equiv.set.insert_symm_apply_inl

added theorem equiv.set.insert_symm_apply_inr

added theorem equiv.set.sum_compl_apply_inl

added theorem equiv.set.sum_compl_apply_inr

added theorem equiv.set.sum_compl_symm_apply

added theorem equiv.set.sum_compl_symm_apply_compl

added theorem equiv.set.sum_compl_symm_apply_of_mem

added theorem equiv.set.sum_compl_symm_apply_of_not_mem

added theorem equiv.set.sum_diff_subset_apply_inl

added theorem equiv.set.sum_diff_subset_apply_inr

added theorem equiv.set.sum_diff_subset_symm_apply_of_mem

added theorem equiv.set.sum_diff_subset_symm_apply_of_not_mem

added theorem equiv.set.union_apply_left

added theorem equiv.set.union_apply_right

added theorem equiv.set.union_symm_apply_left

added theorem equiv.set.union_symm_apply_right

added def equiv.set_congr

added def equiv.set_prod_equiv_sigma

added theorem equiv.symm_image_image

added theorem equiv.symm_preimage_preimage

added theorem set.image_equiv_eq_preimage_symm

added theorem set.mem_image_equiv

added theorem set.preimage_equiv_eq_image_symm

Modified src/data/part.lean

Modified src/logic/embedding.lean

Modified src/logic/small.lean

Modified src/order/order_dual.lean

Modified src/order/rel_iso.lean