Documentation Verification Report

M

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

Statistics

Metric	Count
Definitions `inhabited`, `corec`, `corec'`, `corecContents`, `corecShape`, `dest`, `dest'`, `mk`, `pathDestLeft`, `pathDestRight`, `castDropB`, `castLastB`, `inhabitedM`, `mp`, `mvfunctorM`	15
Theorems `bisim`, `bisim'`, `bisim_lemma`, `bisim₀`, `dest'_eq_dest'`, `dest_corec`, `dest_corec'`, `dest_eq_dest'`, `dest_map`, `map_dest`	10
Total	25

MvPFunctor

Definitions

Name	Category	Theorems
`castDropB` 📖	CompOp	—
`castLastB` 📖	CompOp	—
`inhabitedM` 📖	CompOp	—
`mp` 📖	CompOp	1 math math: `M.dest_eq_dest'`
`mvfunctorM` 📖	CompOp	1 math math: `M.dest_map`

MvPFunctor.M

Definitions

Name	Category	Theorems
`corec` 📖	CompOp	—
`corec'` 📖	CompOp	1 math math: `dest_corec'`
`corecContents` 📖	CompOp	—
`corecShape` 📖	CompOp	—
`dest` 📖	CompOp	6 math math: `dest_eq_dest'`, `dest_map`, `dest_corec`, `map_dest`, `dest_corec'`, `MvQPF.corecF_eq`
`dest'` 📖	CompOp	2 math math: `dest'_eq_dest'`, `dest_eq_dest'`
`mk` 📖	CompOp	—
`pathDestLeft` 📖	CompOp	1 math math: `bisim_lemma`
`pathDestRight` 📖	CompOp	1 math math: `bisim_lemma`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bisim` 📖	—	`dest` `MvPFunctor.A` `TypeVec.Arrow` `MvPFunctor.B` `TypeVec.append1` `MvPFunctor.M` `TypeVec.splitFun`	—	—	`PFunctor.M.bisim` `bisim_lemma` `TypeVec.Arrow.ext`
`bisim'` 📖	—	`MvFunctor.map` `MvPFunctor.Obj` `MvPFunctor.instMvFunctorObj` `TypeVec.append1` `MvPFunctor.M` `TypeVec.appendFun` `TypeVec.id` `dest`	—	—	`bisim₀` `Relation.EqvGen.is_equivalence` `Quot.factor_mk_eq` `TypeVec.appendFun_comp_id` `MvFunctor.map_map` `MvPFunctor.instLawfulMvFunctorObj`
`bisim_lemma` 📖	mathematical	`dest` `MvPFunctor.A` `MvPFunctor.mp` `TypeVec.Arrow` `MvPFunctor.B` `TypeVec.append1` `MvPFunctor.M` `TypeVec.splitFun`	`pathDestLeft` `pathDestRight`	—	`dest_eq_dest'`
`bisim₀` 📖	—	`MvPFunctor.M` `MvFunctor.map` `MvPFunctor.Obj` `MvPFunctor.instMvFunctorObj` `TypeVec.append1` `TypeVec.appendFun` `TypeVec.id` `dest`	—	—	`bisim` `MvPFunctor.map_eq` `TypeVec.split_dropFun_lastFun` `Quot.eqvGen_exact` `Equivalence.eqvGen_iff`
`dest'_eq_dest'` 📖	mathematical	`PFunctor.M.dest` `MvPFunctor.last` `PFunctor.A`	`dest'`	—	—
`dest_corec` 📖	mathematical	—	`dest` `MvFunctor.map` `MvPFunctor.Obj` `MvPFunctor.instMvFunctorObj` `TypeVec.append1` `MvPFunctor.M` `TypeVec.appendFun` `TypeVec.id`	—	`dest_corec'` `MvPFunctor.map_eq` `TypeVec.split_dropFun_lastFun` `TypeVec.appendFun_comp_splitFun`
`dest_corec'` 📖	mathematical	—	`dest` `corec'` `MvPFunctor.A` `TypeVec.Arrow` `MvPFunctor.B` `TypeVec.append1` `MvPFunctor.M` `TypeVec.splitFun` `TypeVec.last`	—	—
`dest_eq_dest'` 📖	mathematical	`PFunctor.M.dest` `MvPFunctor.last` `PFunctor.A`	`dest` `MvPFunctor.A` `MvPFunctor.mp` `TypeVec.Arrow` `MvPFunctor.B` `dest'`	—	`dest'_eq_dest'`
`dest_map` 📖	mathematical	—	`dest` `MvFunctor.map` `MvPFunctor.M` `MvPFunctor.mvfunctorM` `MvPFunctor.Obj` `MvPFunctor.instMvFunctorObj` `TypeVec.append1` `TypeVec.appendFun`	—	`MvPFunctor.map_eq` `dest.eq_1` `dest'.eq_1` `TypeVec.appendFun_comp_splitFun`
`map_dest` 📖	mathematical	`TypeVec.lastFun` `TypeVec.append1` `MvPFunctor.M` `MvFunctor.map` `MvPFunctor.mvfunctorM` `TypeVec.drop` `TypeVec.dropFun`	`MvPFunctor.Obj` `MvPFunctor.instMvFunctorObj` `dest`	—	`dest_map` `TypeVec.eq_of_drop_last_eq`

MvPFunctor.M.Path

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—

---

← Back to Index