Mathlib v3 is deprecated. Go to Mathlib v4

Theorem equiv.apply_inverse_apply

Modification history

2019-03-08 15:01
src/data/equiv/basic.lean
refactot(data/equiv/basic): rename apply_inverse_apply to apply_symm_apply (#800)
Deleted equiv.apply_inverse_applyView on Github →
2017-11-30 22:10
data/equiv.lean
feat(data/analysis): calculations with filters / topologies + misc
Modified equiv.apply_inverse_applyView on Github →
2017-11-23 23:33
data/equiv.lean
feat(data/finset): fintype, multiset.sort, list.pmap
Modified equiv.apply_inverse_applyView on Github →
2017-10-24 22:31
data/equiv.lean
feat(data/num,data/nat/cast,...): nat,num,int,rat.cast, list stuff
Added equiv.apply_inverse_applyView on Github →