Documentation Verification Report

Multivariate

📁 Source: Mathlib/Control/Functor/Multivariate.lean

Statistics

Metric	Count
Definitions `LawfulMvFunctor`, `MvFunctor`, `LiftP`, `LiftP'`, `LiftR`, `LiftR'`, `map`, `ofEquiv`, `supp`, `«term_<$$>_»`	10
Theorems `comp_map`, `id_map`, `LiftP_PredLast_iff`, `LiftP_def`, `LiftR_RelLast_iff`, `LiftR_def`, `exists_iff_exists_of_mono`, `id_map`, `id_map'`, `map_map`, `of_mem_supp`	11
Total	21

LawfulMvFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_map` 📖	mathematical	—	`MvFunctor.map` `TypeVec.comp`	—	—
`id_map` 📖	mathematical	—	`MvFunctor.map` `TypeVec.id`	—	—

MvFunctor

Definitions

Name	Category	Theorems
`LiftP` 📖	MathDef	6 math math: `MvQPF.has_good_supp_iff`, `MvPFunctor.liftP_iff'`, `MvPFunctor.liftP_iff`, `MvQPF.liftP_iff`, `MvQPF.liftP_iff_of_isUniform`, `LiftP_PredLast_iff`
`LiftP'` 📖	MathDef	2 math math: `LiftP_def`, `LiftP_PredLast_iff`
`LiftR` 📖	MathDef	3 math math: `LiftR_RelLast_iff`, `MvQPF.liftR_iff`, `MvPFunctor.liftR_iff`
`LiftR'` 📖	MathDef	5 math math: `MvQPF.liftR_map_last'`, `LiftR_RelLast_iff`, `MvQPF.liftR_map_last`, `LiftR_def`, `MvQPF.liftR_map`
`map` 📖	CompOp	35 math math: `MvPFunctor.id_map`, `LawfulMvFunctor.id_map`, `MvQPF.liftR_map_last'`, `LawfulMvFunctor.comp_map`, `MvQPF.comp_map`, `id_map`, `id_map'`, `MvQPF.liftR_map_last`, `LiftP_def`, `MvPFunctor.comp.get_map`, `MvQPF.Cofix.dest_corec'`, `MvPFunctor.w_map_wMk`, `MvQPF.recF_eq'`, `MvPFunctor.map_eq`, `MvQPF.Cofix.dest_corec`, `MvPFunctor.comp_map`, `MvQPF.Comp.get_map`, `MvQPF.Comp.map_mk`, `LiftR_def`, `MvPFunctor.M.dest_map`, `MvPFunctor.M.dest_corec`, `MvQPF.corec_roll`, `MvQPF.Const.map_mk`, `MvPFunctor.map_objAppend1`, `MvQPF.id_map`, `MvQPF.wrepr_wMk`, `MvQPF.liftR_map`, `MvQPF.supp_map`, `MvQPF.abs_map`, `MvQPF.Const.get_map`, `MvQPF.corecF_eq`, `MvQPF.wEquiv_map`, `MvPFunctor.const.get_map`, `MvQPF.Fix.rec_eq`, `map_map`
`ofEquiv` 📖	CompOp	—
`supp` 📖	CompOp	5 math math: `MvQPF.supp_eq`, `MvQPF.mem_supp`, `MvPFunctor.supp_eq`, `MvQPF.supp_eq_of_isUniform`, `MvQPF.supp_map`
`«term_<$$>_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LiftP_PredLast_iff` 📖	mathematical	—	`LiftP'` `TypeVec.append1` `TypeVec.PredLast'` `LiftP` `TypeVec.PredLast`	—	`exists_iff_exists_of_mono` `TypeVec.Arrow.ext` `map_map`
`LiftP_def` 📖	mathematical	—	`LiftP'` `map` `TypeVec.Subtype_` `TypeVec.subtypeVal`	—	`exists_iff_exists_of_mono` `TypeVec.toSubtype_of_subtype` `map_map` `TypeVec.subtypeVal_toSubtype`
`LiftR_RelLast_iff` 📖	mathematical	—	`LiftR'` `TypeVec.append1` `TypeVec.RelLast'` `LiftR` `TypeVec.RelLast`	—	`exists_iff_exists_of_mono` `TypeVec.Arrow.ext` `map_map`
`LiftR_def` 📖	mathematical	—	`LiftR'` `map` `TypeVec.Subtype_` `TypeVec.prod` `TypeVec.comp` `TypeVec.prod.fst` `TypeVec.subtypeVal` `TypeVec.prod.snd`	—	`exists_iff_exists_of_mono` `TypeVec.toSubtype'_of_subtype'` `map_map` `TypeVec.subtypeVal_toSubtype'`
`exists_iff_exists_of_mono` 📖	—	`TypeVec.comp` `TypeVec.id` `map`	—	—	`map_map` `LawfulMvFunctor.id_map`
`id_map` 📖	mathematical	—	`map` `TypeVec.id`	—	`LawfulMvFunctor.id_map`
`id_map'` 📖	mathematical	—	`map`	—	`id_map`
`map_map` 📖	mathematical	—	`map` `TypeVec.comp`	—	`LawfulMvFunctor.comp_map`
`of_mem_supp` 📖	—	`LiftP` `Set` `Set.instMembership` `supp`	—	—	—

(root)

Definitions

Name	Category	Theorems
`LawfulMvFunctor` 📖	CompData	2 math math: `MvQPF.lawfulMvFunctor`, `MvPFunctor.instLawfulMvFunctorObj`
`MvFunctor` 📖	CompData	—

---

← Back to Index