Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-14 15:25 7e9094b1

View on Github →

feat(control/equiv_functor): simp defn lemmas and injectivity (#5739)

Estimated changes

Modified src/control/equiv_functor.lean

added theorem equiv_functor.map_equiv.injective

added theorem equiv_functor.map_equiv_refl

added theorem equiv_functor.map_equiv_symm

modified theorem equiv_functor.map_equiv_symm_apply

added theorem equiv_functor.map_equiv_trans