Commit 2023-02-20 13:00 eab0a098

View on Github →

feat: Port Data.PFunctor.Multivariate.W (#2233)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/PFunctor/Multivariate/W.lean

added def MvPFunctor.W

added inductive MvPFunctor.WPath

added theorem MvPFunctor.comp_wPathCasesOn

added theorem MvPFunctor.map_objAppend1

added def MvPFunctor.objAppend1

added def MvPFunctor.wDest'

added theorem MvPFunctor.wDest'_wMk'

added theorem MvPFunctor.wDest'_wMk

added def MvPFunctor.wMap

added def MvPFunctor.wMk'

added def MvPFunctor.wMk

added theorem MvPFunctor.wMk_eq

added def MvPFunctor.wPathCasesOn

added theorem MvPFunctor.wPathCasesOn_eta

added def MvPFunctor.wPathDestLeft

added theorem MvPFunctor.wPathDestLeft_wPathCasesOn

added def MvPFunctor.wPathDestRight

added theorem MvPFunctor.wPathDestRight_wPathCasesOn

added def MvPFunctor.wRec

added theorem MvPFunctor.wRec_eq

added theorem MvPFunctor.w_cases

added theorem MvPFunctor.w_ind

added theorem MvPFunctor.w_map_wMk

added def MvPFunctor.wp

added def MvPFunctor.wpMk

added def MvPFunctor.wpRec

added theorem MvPFunctor.wpRec_eq

added theorem MvPFunctor.wp_ind