Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-05 22:33 0db59dbf

View on Github →

feat(data/equiv/basic): some elementary equivs (#2602)

Estimated changes

Modified src/data/equiv/basic.lean

added def equiv.fun_unique

added theorem equiv.fun_unique_apply

added theorem equiv.fun_unique_symm_apply

added theorem equiv.sigma_preimage_equiv_apply

added theorem equiv.sigma_preimage_equiv_symm_apply_fst

added theorem equiv.sigma_preimage_equiv_symm_apply_snd_fst

added def equiv.subtype_preimage

added theorem equiv.subtype_preimage_apply

added theorem equiv.subtype_preimage_symm_apply_coe

added theorem equiv.subtype_preimage_symm_apply_coe_neg

added theorem equiv.subtype_preimage_symm_apply_coe_pos

added def equiv.sum_compl

added theorem equiv.sum_compl_apply_inl

added theorem equiv.sum_compl_apply_inr

added theorem equiv.sum_compl_apply_symm_of_neg

added theorem equiv.sum_compl_apply_symm_of_pos