Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-26 10:52 0444f9c2

View on Github →

feat(data/equiv/basic): sum_compl_apply and others (#961)

feat(data/equiv/basic): sum_congr_apply and others
Update basic.lean

Estimated changes

Modified src/data/equiv/basic.lean

added theorem equiv.set.of_eq_apply

added theorem equiv.set.of_eq_symm_apply

added theorem equiv.set.sum_compl_apply_inl

added theorem equiv.set.sum_compl_apply_inr

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

added theorem equiv.set.union_apply_right

added theorem equiv.set.univ_apply

added theorem equiv.set.univ_symm_apply

added theorem equiv.symm_symm_apply