EquivFunctor
instances #
We derive some EquivFunctor
instances, to enable equiv_rw
to rewrite under these functions.
Equations
- EquivFunctorUnique = EquivFunctor.mk fun {α β} e => ↑(Equiv.uniqueCongr e)
Equations
- EquivFunctorPerm = EquivFunctor.mk fun {α β} e p => Equiv.trans (Equiv.trans (Equiv.symm e) p) e
Equations
- EquivFunctorFinset = EquivFunctor.mk fun {α β} e s => Finset.map (Equiv.toEmbedding e) s
Equations
- EquivFunctorFintype = EquivFunctor.mk fun {α β} e s => Fintype.ofBijective ↑e (_ : Function.Bijective ↑e)