Fix

📁 Source: Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean

Statistics

Metric	Count
Definitions Fix, Fix, dest, drec, map, mk, mvfunctor, rec, WEquiv, fixToW, mvqpfFix, recF, wSetoid, wrepr, Fix	15
Theorems dest_mk, ind, ind_aux, ind_rec, mk_dest, rec_eq, rec_unique, recF_eq, recF_eq', recF_eq_of_wEquiv, abs', refl, wEquiv_map, wrepr_equiv, wrepr_wMk	15
Total	30

MvQPF

Definitions

Name	Category	Theorems
Fix 📖	CompOp	2 math math: Fix.ind_aux, Fix.rec_eq
WEquiv 📖	CompData	3 math math: wEquiv.refl, wEquiv.abs', wrepr_equiv
fixToW 📖	CompOp	—
mvqpfFix 📖	CompOp	—
recF 📖	CompOp	3 math math: recF_eq', recF_eq_of_wEquiv, recF_eq
wSetoid 📖	CompOp	1 math math: Fix.ind_aux
wrepr 📖	CompOp	2 math math: wrepr_equiv, wrepr_wMk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
recF_eq 📖	mathematical	—	recF MvPFunctor.wMk P abs TypeVec.append1 MvPFunctor.A TypeVec.Arrow MvPFunctor.B TypeVec.splitFun TypeVec.last MvPFunctor.W	—	recF.eq_1 MvPFunctor.wRec_eq
recF_eq' 📖	mathematical	—	recF abs TypeVec.append1 MvFunctor.map MvPFunctor.Obj P MvPFunctor.instMvFunctorObj MvPFunctor.W TypeVec.appendFun TypeVec.id MvPFunctor.wDest'	—	MvPFunctor.w_cases recF_eq MvPFunctor.wDest'_wMk MvPFunctor.map_eq TypeVec.appendFun_comp_splitFun TypeVec.id_comp
recF_eq_of_wEquiv 📖	mathematical	WEquiv	recF	—	MvPFunctor.w_cases recF_eq recF_eq' MvPFunctor.wDest'_wMk abs_map
wEquiv_map 📖	mathematical	WEquiv	MvFunctor.map MvPFunctor.W P MvPFunctor.mvfunctorW	—	MvPFunctor.w_map_wMk MvPFunctor.map_objAppend1 abs_map
wrepr_equiv 📖	mathematical	—	WEquiv wrepr	—	MvPFunctor.w_ind wEquiv.abs' wrepr_wMk MvPFunctor.wDest'_wMk' abs_repr MvPFunctor.map_eq MvPFunctor.wMk'.eq_1 TypeVec.appendFun_comp_splitFun TypeVec.id_comp
wrepr_wMk 📖	mathematical	—	wrepr MvPFunctor.wMk P MvPFunctor.wMk' repr TypeVec.append1 MvPFunctor.W abs MvFunctor.map MvPFunctor.Obj MvPFunctor.instMvFunctorObj TypeVec.appendFun TypeVec.id MvPFunctor.A TypeVec.Arrow MvPFunctor.B MvPFunctor.appendContents	—	wrepr.eq_1 recF_eq' MvPFunctor.wDest'_wMk

MvQPF.Fix

Definitions

Name	Category	Theorems
dest 📖	CompOp	2 math math: mk_dest, dest_mk
drec 📖	CompOp	—
map 📖	CompOp	—
mk 📖	CompOp	—
mvfunctor 📖	CompOp	—
rec 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dest_mk 📖	mathematical	—	dest	—	rec_eq dest.eq_1 MvQPF.comp_map MvFunctor.id_map MvQPF.lawfulMvFunctor TypeVec.appendFun_comp TypeVec.id_comp mk_dest TypeVec.appendFun_id_id
ind 📖	—	—	—	—	MvPFunctor.w_ind ind_aux MvQPF.liftP_iff
ind_aux 📖	mathematical	—	MvQPF.abs TypeVec.append1 MvQPF.Fix MvPFunctor.A MvQPF.P TypeVec.Arrow MvPFunctor.B MvPFunctor.appendContents MvPFunctor.W MvQPF.wSetoid MvPFunctor.wMk	—	MvQPF.wEquiv.abs' MvPFunctor.wDest'_wMk' MvQPF.abs_map MvQPF.abs_repr MvPFunctor.map_eq MvQPF.wrepr_wMk MvPFunctor.appendContents.eq_1 TypeVec.appendFun.eq_1 TypeVec.splitFun_comp MvQPF.wrepr_equiv
ind_rec 📖	—	—	—	—	MvPFunctor.w_ind ind_aux MvQPF.abs_map MvPFunctor.map_eq MvPFunctor.appendContents.eq_1 TypeVec.appendFun.eq_1 TypeVec.splitFun_comp
mk_dest 📖	mathematical	—	dest	—	dest.eq_1 rec_eq MvQPF.comp_map TypeVec.appendFun_comp TypeVec.id_comp TypeVec.appendFun_id_id MvFunctor.id_map MvQPF.lawfulMvFunctor
rec_eq 📖	mathematical	—	MvFunctor.map MvQPF.toMvFunctor TypeVec.append1 MvQPF.Fix TypeVec.appendFun TypeVec.id	—	MvQPF.recF_eq_of_wEquiv MvQPF.wrepr_equiv MvPFunctor.map_eq MvQPF.recF_eq' MvPFunctor.wDest'_wMk' MvPFunctor.comp_map MvQPF.abs_map MvQPF.abs_repr TypeVec.appendFun_comp TypeVec.id_comp
rec_unique 📖	—	MvFunctor.map MvQPF.toMvFunctor TypeVec.append1 MvQPF.Fix TypeVec.appendFun TypeVec.id	—	—	rec_eq

MvQPF.wEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs' 📖	mathematical	MvQPF.abs TypeVec.append1 MvPFunctor.W MvQPF.P MvPFunctor.wDest'	MvQPF.WEquiv	—	MvPFunctor.w_cases
refl 📖	mathematical	—	MvQPF.WEquiv	—	abs'

QPF

Definitions

Name	Category	Theorems
Fix 📖	CompOp	2 math math: Fix.ind_aux, Fix.rec_eq

(root)

Definitions

Name	Category	Theorems
Fix 📖	CompData	—

---

← Back to Index