Documentation Verification Report

Two

📁 Source: Mathlib/CategoryTheory/ComposableArrows/Two.lean

Statistics

Metric	Count
Definitions `twoδ₁Toδ₀`, `twoδ₁Toδ₀'`, `twoδ₂Toδ₁`, `twoδ₂Toδ₁'`	4
Theorems `instIsIsoOfNatNatTwoδ₁Toδ₀`, `instIsIsoOfNatNatTwoδ₂Toδ₁`, `twoδ₁Toδ₀_app_one`, `twoδ₁Toδ₀_app_zero`, `twoδ₂Toδ₁_app_one`, `twoδ₂Toδ₁_app_zero`	6
Total	10

CategoryTheory.ComposableArrows

Definitions

Name	Category	Theorems
`twoδ₁Toδ₀` 📖	CompOp	4 math math: `twoδ₁Toδ₀_app_zero`, `CategoryTheory.Triangulated.SpectralObject.triangle_mor₂`, `twoδ₁Toδ₀_app_one`, `instIsIsoOfNatNatTwoδ₁Toδ₀`
`twoδ₁Toδ₀'` 📖	CompOp	—
`twoδ₂Toδ₁` 📖	CompOp	4 math math: `twoδ₂Toδ₁_app_zero`, `CategoryTheory.Triangulated.SpectralObject.triangle_mor₁`, `twoδ₂Toδ₁_app_one`, `instIsIsoOfNatNatTwoδ₂Toδ₁`
`twoδ₂Toδ₁'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsIsoOfNatNatTwoδ₁Toδ₀` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.IsIso` `CategoryTheory.ComposableArrows` `CategoryTheory.Functor.category` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `mk₁` `twoδ₁Toδ₀`	—	`isIso_iff₁` `CategoryTheory.IsIso.id`
`instIsIsoOfNatNatTwoδ₂Toδ₁` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.IsIso` `CategoryTheory.ComposableArrows` `CategoryTheory.Functor.category` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `mk₁` `twoδ₂Toδ₁`	—	`isIso_iff₁` `CategoryTheory.IsIso.id`
`twoδ₁Toδ₀_app_one` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.NatTrans.app` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `mk₁` `twoδ₁Toδ₀` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor.obj`	—	—
`twoδ₁Toδ₀_app_zero` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.NatTrans.app` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `mk₁` `twoδ₁Toδ₀`	—	—
`twoδ₂Toδ₁_app_one` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.NatTrans.app` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `mk₁` `twoδ₂Toδ₁`	—	—
`twoδ₂Toδ₁_app_zero` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.NatTrans.app` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `mk₁` `twoδ₂Toδ₁` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor.obj`	—	—

---

← Back to Index