Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `PFunctor`, `A`, `B`, `Idx`, `inhabited`, `Obj`, `iget`, `inhabited`, `children`, `dest`, `head`, `mk`, `comp`, `get`, `mk`, `instCoeFunForallType`, `instFunctorObj`, `instInhabited`, `map`	19
Theorems `dest_mk`, `mk_dest`, `fst_map`, `id_map`, `iget_map`, `instLawfulFunctorObj`, `liftp_iff`, `liftp_iff'`, `liftr_iff`, `map_eq`, `map_eq_map`, `map_map`, `supp_eq`	13
Total	32

PFunctor

Definitions

Name	Category	Theorems
`A` 📖	CompOp	25 math math: `QPF.liftp_iff'`, `M.head_mk`, `supp_eq`, `QPF.recF_eq'`, `MvPFunctor.wpRec_eq`, `QPF.Fix.ind_aux`, `M.casesOn_mk'`, `MvPFunctor.wMk_eq`, `fst_map`, `M.iselect_nil`, `MvPFunctor.comp_wPathCasesOn`, `M.approx_mk`, `liftp_iff`, `M.children_mk`, `QPF.has_good_supp_iff`, `QPF.liftr_iff`, `QPF.supp_eq_of_isUniform`, `liftr_iff`, `liftp_iff'`, `MvPFunctor.M.bisim_lemma`, `M.iselect_cons`, `QPF.liftp_iff`, `map_eq`, `M.isubtree_cons`, `M.nth_of_bisim`
`B` 📖	CompOp	13 math math: `supp_eq`, `QPF.recF_eq'`, `MvPFunctor.wpRec_eq`, `QPF.Fix.ind_aux`, `MvPFunctor.wMk_eq`, `MvPFunctor.comp_wPathCasesOn`, `QPF.mem_supp`, `M.children_mk`, `QPF.has_good_supp_iff`, `QPF.supp_eq_of_isUniform`, `M.iselect_cons`, `map_eq`, `M.isubtree_cons`
`Idx` 📖	CompOp	3 math math: `M.iselect_nil`, `M.iselect_cons`, `M.isubtree_cons`
`Obj` 📖	CompOp	8 math math: `QPF.liftp_iff'`, `instLawfulFunctorObj`, `supp_eq`, `liftp_iff`, `liftr_iff`, `liftp_iff'`, `MvPFunctor.M.bisim_lemma`, `map_eq_map`
`comp` 📖	CompOp	—
`instCoeFunForallType` 📖	CompOp	—
`instFunctorObj` 📖	CompOp	6 math math: `instLawfulFunctorObj`, `supp_eq`, `liftp_iff`, `liftr_iff`, `liftp_iff'`, `map_eq_map`
`instInhabited` 📖	CompOp	—
`map` 📖	CompOp	12 math math: `QPF.recF_eq'`, `map_map`, `QPF.abs_map`, `fst_map`, `QPF.corecF_eq`, `M.corec_def`, `iget_map`, `id_map`, `QPF.recF_eq`, `M.dest_corec`, `map_eq_map`, `map_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst_map` 📖	mathematical	—	`A` `map`	—	—
`id_map` 📖	mathematical	—	`map`	—	—
`iget_map` 📖	mathematical	`A` `B`	`Obj.iget` `map`	—	`fst_map`
`instLawfulFunctorObj` 📖	mathematical	—	`Obj` `instFunctorObj`	—	`id_map` `map_map`
`liftp_iff` 📖	mathematical	—	`Functor.Liftp` `Obj` `instFunctorObj` `A`	—	`map_eq_map` `map_eq`
`liftp_iff'` 📖	mathematical	—	`Functor.Liftp` `Obj` `instFunctorObj` `A`	—	—
`liftr_iff` 📖	mathematical	—	`Functor.Liftr` `Obj` `instFunctorObj` `A`	—	—
`map_eq` 📖	mathematical	—	`map` `A` `B`	—	—
`map_eq_map` 📖	mathematical	—	`Obj` `instFunctorObj` `map`	—	—
`map_map` 📖	mathematical	—	`map`	—	—
`supp_eq` 📖	mathematical	—	`Functor.supp` `Obj` `instFunctorObj` `A` `Set.image` `B` `Set.univ`	—	`Set.ext` `Set.image_univ` `liftp_iff'`

PFunctor.Idx

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—

PFunctor.Obj

Definitions

Name	Category	Theorems
`iget` 📖	CompOp	2 math math: `PFunctor.M.ichildren_mk`, `PFunctor.iget_map`
`inhabited` 📖	CompOp	—

PFunctor.W

Definitions

Name	Category	Theorems
`children` 📖	CompOp	—
`dest` 📖	CompOp	3 math math: `mk_dest`, `dest_mk`, `QPF.recF_eq`
`head` 📖	CompOp	—
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dest_mk` 📖	mathematical	—	`dest`	—	—
`mk_dest` 📖	mathematical	—	`dest`	—	—

PFunctor.comp

Definitions

Name	Category	Theorems
`get` 📖	CompOp	—
`mk` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`PFunctor` 📖	CompData	—

---

← Back to Index