Commit 2023-01-24 19:47 38c9db93

View on Github →

feat: port Control.Functor.Multivariate (#1638)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Control/Functor/Multivariate.lean

added def MvFunctor.LiftP'

added def MvFunctor.LiftP

added theorem MvFunctor.LiftP_PredLast_iff

added theorem MvFunctor.LiftP_def

added def MvFunctor.LiftR'

added def MvFunctor.LiftR

added theorem MvFunctor.LiftR_RelLast_iff

added theorem MvFunctor.LiftR_def

added theorem MvFunctor.exists_iff_exists_of_mono

added theorem MvFunctor.id_map'

added theorem MvFunctor.id_map

added theorem MvFunctor.map_map

added theorem MvFunctor.of_mem_supp

added def MvFunctor.supp

Modified Mathlib/Data/TypeVec.lean

added def TypeVec.PredLast'

added def TypeVec.RelLast'

added theorem TypeVec.dropFun_RelLast'

deleted theorem TypeVec.dropFun_rel_last

deleted def TypeVec.predLast'

deleted def TypeVec.relLast'