Documentation Verification Report

Cofix

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

Statistics

Metric	Count
Definitions `tacticMv_bisim___With___`, `Cofix`, `abs`, `corec`, `corec'`, `corec'₁`, `corec₁`, `dest`, `map`, `mk`, `mvfunctor`, `repr`, `IsPrecongr`, `Mcongr`, `corecF`, `instInhabitedCofixOfAP`, `mRepr`, `mvqpfCofix`, `Cofix`	19
Theorems `abs_repr`, `bisim`, `bisim'`, `bisim_rel`, `bisim₂`, `dest_corec`, `dest_corec'`, `dest_corec₁`, `dest_mk`, `ext`, `ext_mk`, `mk_dest`, `corecF_eq`, `corec_roll`, `liftR_map`, `liftR_map_last`, `liftR_map_last'`	17
Total	36

Mathlib.Tactic.MvBisim

Definitions

Name	Category	Theorems
`tacticMv_bisim___With___` 📖	CompOp	—

MvQPF

Definitions

Name	Category	Theorems
`Cofix` 📖	CompOp	2 math math: `Cofix.dest_corec'`, `Cofix.dest_corec`
`IsPrecongr` 📖	MathDef	—
`Mcongr` 📖	MathDef	1 math math: `Cofix.abs_repr`
`corecF` 📖	CompOp	1 math math: `corecF_eq`
`instInhabitedCofixOfAP` 📖	CompOp	—
`mRepr` 📖	CompOp	—
`mvqpfCofix` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`corecF_eq` 📖	mathematical	—	`MvPFunctor.M.dest` `P` `corecF` `MvFunctor.map` `MvPFunctor.Obj` `MvPFunctor.instMvFunctorObj` `TypeVec.append1` `MvPFunctor.M` `TypeVec.appendFun` `TypeVec.id` `repr`	—	`corecF.eq_1`
`corec_roll` 📖	mathematical	—	`TypeVec.append1` `MvFunctor.map` `toMvFunctor` `TypeVec.appendFun` `TypeVec.id`	—	`Cofix.bisim₂` `MvFunctor.map_map` `lawfulMvFunctor` `TypeVec.appendFun_comp_id` `liftR_map_last`
`liftR_map` 📖	mathematical	`TypeVec.comp` `TypeVec.Subtype_` `TypeVec.prod` `TypeVec.subtypeVal` `TypeVec.prod.map` `TypeVec.prod.diag`	`MvFunctor.LiftR'` `MvFunctor.map`	—	`MvFunctor.LiftR_def` `MvFunctor.map_map` `TypeVec.comp_assoc` `TypeVec.fst_diag` `TypeVec.snd_diag`
`liftR_map_last` 📖	mathematical	—	`MvFunctor.LiftR'` `TypeVec.append1` `toMvFunctor` `TypeVec.RelLast'` `MvFunctor.map` `TypeVec.appendFun` `TypeVec.id`	—	`TypeVec.eq_of_drop_last_eq` `TypeVec.prod_map_id` `TypeVec.toSubtype_of_subtype_assoc` `TypeVec.id_comp` `TypeVec.Arrow.ext` `liftR_map`
`liftR_map_last'` 📖	mathematical	—	`MvFunctor.LiftR'` `TypeVec.append1` `toMvFunctor` `TypeVec.RelLast'` `MvFunctor.map` `TypeVec.appendFun` `TypeVec.id`	—	`liftR_map_last` `MvFunctor.id_map` `TypeVec.appendFun_id_id`

MvQPF.Cofix

Definitions

Name	Category	Theorems
`abs` 📖	CompOp	—
`corec` 📖	CompOp	—
`corec'` 📖	CompOp	1 math math: `dest_corec'`
`corec'₁` 📖	CompOp	—
`corec₁` 📖	CompOp	1 math math: `dest_corec₁`
`dest` 📖	CompOp	5 math math: `dest_corec₁`, `dest_corec'`, `dest_corec`, `mk_dest`, `dest_mk`
`map` 📖	CompOp	—
`mk` 📖	CompOp	—
`mvfunctor` 📖	CompOp	—
`repr` 📖	CompOp	1 math math: `abs_repr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_repr` 📖	mathematical	—	`MvPFunctor.M` `MvQPF.P` `MvQPF.Mcongr` `repr`	—	`bisim₂` `MvQPF.abs_map` `MvQPF.abs_repr` `dest.eq_1` `MvFunctor.map_map` `MvQPF.lawfulMvFunctor` `TypeVec.appendFun_comp_id` `MvQPF.liftR_map_last`
`bisim` 📖	—	`MvFunctor.LiftR` `MvQPF.toMvFunctor` `TypeVec.append1` `MvQPF.Cofix` `TypeVec.RelLast` `dest`	—	—	`bisim_rel` `MvQPF.liftR_iff` `MvQPF.abs_map` `MvPFunctor.map_eq` `TypeVec.split_dropFun_lastFun` `TypeVec.appendFun_comp_splitFun` `TypeVec.id_comp` `TypeVec.Arrow.ext`
`bisim'` 📖	—	`dest` `MvQPF.abs` `TypeVec.append1` `MvQPF.Cofix` `MvPFunctor.A` `MvQPF.P` `TypeVec.Arrow` `MvPFunctor.B` `MvPFunctor.appendContents`	—	—	`bisim` `MvQPF.liftR_iff`
`bisim_rel` 📖	—	`MvFunctor.map` `MvQPF.toMvFunctor` `TypeVec.append1` `MvQPF.Cofix` `TypeVec.appendFun` `TypeVec.id` `dest`	—	—	`Quot.factor_mk_eq` `TypeVec.appendFun_comp_id` `MvQPF.comp_map`
`bisim₂` 📖	—	`MvFunctor.LiftR'` `TypeVec.append1` `MvQPF.Cofix` `MvQPF.toMvFunctor` `TypeVec.RelLast'` `dest`	—	—	`bisim` `MvFunctor.LiftR_RelLast_iff` `MvQPF.lawfulMvFunctor`
`dest_corec` 📖	mathematical	—	`dest` `MvFunctor.map` `MvQPF.toMvFunctor` `TypeVec.append1` `MvQPF.Cofix` `TypeVec.appendFun` `TypeVec.id`	—	`dest.eq_1` `corec.eq_1` `MvQPF.corecF_eq` `MvQPF.abs_map` `MvQPF.abs_repr` `MvQPF.comp_map` `TypeVec.appendFun_comp`
`dest_corec'` 📖	mathematical	—	`dest` `corec'` `MvFunctor.map` `MvQPF.toMvFunctor` `TypeVec.append1` `MvQPF.Cofix` `TypeVec.appendFun` `TypeVec.id`	—	`corec'.eq_1` `MvQPF.corec_roll` `bisim₂` `MvFunctor.map_map` `MvQPF.lawfulMvFunctor` `TypeVec.appendFun_comp_id` `MvQPF.liftR_map_last'` `TypeVec.appendFun_id_id` `MvFunctor.id_map`
`dest_corec₁` 📖	mathematical	`MvQPF.Cofix` `MvFunctor.map` `MvQPF.toMvFunctor` `TypeVec.append1` `TypeVec.appendFun` `TypeVec.id`	`dest` `corec₁`	—	`corec₁.eq_1` `dest_corec'`
`dest_mk` 📖	mathematical	—	`dest`	—	`mk_dest` `MvQPF.comp_map` `TypeVec.appendFun_comp` `TypeVec.id_comp` `TypeVec.appendFun_id_id` `MvFunctor.id_map` `MvQPF.lawfulMvFunctor`
`ext` 📖	—	`dest`	—	—	`mk_dest`
`ext_mk` 📖	—	—	—	—	—
`mk_dest` 📖	mathematical	—	`dest`	—	`bisim_rel` `MvQPF.comp_map` `TypeVec.appendFun_comp` `TypeVec.id_comp`

QPF

Definitions

Name	Category	Theorems
`Cofix` 📖	CompOp	1 math math: `Cofix.dest_corec`

---

← Back to Index