Basic

📁 Source: Mathlib/Data/PFunctor/Multivariate/Basic.lean

Statistics

Metric	Count
Definitions MvPFunctor, A, B, Obj, inhabited, appendContents, comp, get, mk, const, get, mk, drop, instCoeFunForallTypeVecType, instInhabited, instMvFunctorObj, last, map	18
Theorems get_map, get_mk, mk_get, comp_map, get_map, get_mk, mk_get, id_map, instLawfulMvFunctorObj, liftP_iff, liftP_iff', liftR_iff, map_eq, supp_eq	14
Total	32

MvPFunctor

Definitions

Name	Category	Theorems
A 📖	CompOp	16 math math: MvQPF.has_good_supp_iff, wDest'_wMk, wMk_eq, MvQPF.Fix.ind_aux, M.dest_eq_dest', map_eq, supp_eq, MvQPF.liftR_iff, liftP_iff', liftR_iff, MvQPF.wrepr_wMk, M.dest_corec', MvQPF.supp_eq_of_isUniform, liftP_iff, MvQPF.liftP_iff, MvQPF.recF_eq
B 📖	CompOp	20 math math: MvQPF.has_good_supp_iff, wDest'_wMk, wMk_eq, MvQPF.Fix.ind_aux, MvQPF.mem_supp, w_map_wMk, M.dest_eq_dest', map_eq, comp_wPathCasesOn, supp_eq, MvQPF.liftR_iff, liftP_iff', liftR_iff, map_objAppend1, MvQPF.wrepr_wMk, M.dest_corec', MvQPF.supp_eq_of_isUniform, liftP_iff, MvQPF.liftP_iff, MvQPF.recF_eq
Obj 📖	CompOp	18 math math: id_map, comp.get_map, MvQPF.recF_eq', map_eq, comp_map, supp_eq, M.dest_map, liftP_iff', M.dest_corec, liftR_iff, map_objAppend1, MvQPF.wrepr_wMk, M.map_dest, MvQPF.abs_map, liftP_iff, MvQPF.corecF_eq, const.get_map, instLawfulMvFunctorObj
appendContents 📖	CompOp	2 math math: MvQPF.Fix.ind_aux, MvQPF.wrepr_wMk
comp 📖	CompOp	1 math math: comp.get_map
const 📖	CompOp	1 math math: const.get_map
drop 📖	CompOp	3 math math: w_map_wMk, comp_wPathCasesOn, map_objAppend1
instCoeFunForallTypeVecType 📖	CompOp	—
instInhabited 📖	CompOp	—
instMvFunctorObj 📖	CompOp	18 math math: id_map, comp.get_map, MvQPF.recF_eq', map_eq, comp_map, supp_eq, M.dest_map, liftP_iff', M.dest_corec, liftR_iff, map_objAppend1, MvQPF.wrepr_wMk, M.map_dest, MvQPF.abs_map, liftP_iff, MvQPF.corecF_eq, const.get_map, instLawfulMvFunctorObj
last 📖	CompOp	3 math math: wpRec_eq, wMk_eq, comp_wPathCasesOn
map 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_map 📖	mathematical	—	MvFunctor.map Obj instMvFunctorObj TypeVec.comp	—	—
id_map 📖	mathematical	—	MvFunctor.map Obj instMvFunctorObj TypeVec.id	—	—
instLawfulMvFunctorObj 📖	mathematical	—	LawfulMvFunctor Obj instMvFunctorObj	—	id_map comp_map
liftP_iff 📖	mathematical	—	MvFunctor.LiftP Obj instMvFunctorObj A TypeVec.Arrow B	—	map_eq
liftP_iff' 📖	mathematical	—	MvFunctor.LiftP Obj instMvFunctorObj A TypeVec.Arrow B	—	—
liftR_iff 📖	mathematical	—	MvFunctor.LiftR Obj instMvFunctorObj A TypeVec.Arrow B	—	—
map_eq 📖	mathematical	—	MvFunctor.map Obj instMvFunctorObj A TypeVec.Arrow B TypeVec.comp	—	—
supp_eq 📖	mathematical	—	MvFunctor.supp Obj instMvFunctorObj A TypeVec.Arrow B Set.image Set.univ	—	Set.ext Set.image_univ liftP_iff'

MvPFunctor.Obj

Definitions

Name	Category	Theorems
inhabited 📖	CompOp	—

MvPFunctor.comp

Definitions

Name	Category	Theorems
get 📖	CompOp	3 math math: get_map, get_mk, mk_get
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
get_map 📖	mathematical	—	get MvFunctor.map MvPFunctor.Obj MvPFunctor.comp MvPFunctor.instMvFunctorObj	—	—
get_mk 📖	mathematical	—	get	—	—
mk_get 📖	mathematical	—	get	—	—

MvPFunctor.const

Definitions

Name	Category	Theorems
get 📖	CompOp	3 math math: mk_get, get_mk, get_map
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
get_map 📖	mathematical	—	get MvFunctor.map MvPFunctor.Obj MvPFunctor.const MvPFunctor.instMvFunctorObj	—	—
get_mk 📖	mathematical	—	get	—	—
mk_get 📖	mathematical	—	get	—	TypeVec.Arrow.ext

(root)

Definitions

Name	Category	Theorems
MvPFunctor 📖	CompData	—

---

← Back to Index