Commit 2022-12-15 17:55 7495fe35

View on Github →

feat port: Logic.Equiv.Set (#1044) aba57d4d3dae35460225919dcd82fe91355162f9

Estimated changes

Modified Mathlib.lean

Created Mathlib/Logic/Equiv/Set.lean

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.sumCompl_apply_inl

added theorem Equiv.Set.sumCompl_apply_inr

added theorem Equiv.Set.sumCompl_symm_apply

added theorem Equiv.Set.sumCompl_symm_apply_compl

added theorem Equiv.Set.sumCompl_symm_apply_of_mem

added theorem Equiv.Set.sumCompl_symm_apply_of_not_mem

added theorem Equiv.Set.sumDiffSubset_apply_inl

added theorem Equiv.Set.sumDiffSubset_apply_inr

added theorem Equiv.Set.sumDiffSubset_symm_apply_of_mem

added theorem Equiv.Set.sumDiffSubset_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 theorem Equiv.apply_ofInjective_symm

added theorem Equiv.coe_ofInjective_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.ofInjective_symm_apply

added theorem Equiv.ofLeftInverse'_eq_ofInjective

added def Equiv.ofLeftInverse

added theorem Equiv.ofLeftInverse_eq_ofInjective

added def Equiv.ofPreimageEquiv

added theorem Equiv.ofPreimageEquiv_map

added theorem Equiv.preimage_eq_iff_eq_image

added theorem Equiv.preimage_image

added theorem Equiv.preimage_piEquivPiSubtypeProd_symm_pi

added theorem Equiv.preimage_subset

added theorem Equiv.preimage_symm_preimage

added theorem Equiv.prod_assoc_image

added theorem Equiv.prod_assoc_preimage

added theorem Equiv.prod_assoc_symm_image

added theorem Equiv.prod_assoc_symm_preimage

added theorem Equiv.range_eq_univ

added theorem Equiv.self_comp_ofInjective_symm

added def Equiv.setCongr

added def Equiv.setProdEquivSigma

added def Equiv.sigmaPreimageEquiv

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

added theorem dite_comp_equiv_update