Documentation Verification Report

OfSequence

📁 Source: Mathlib/CategoryTheory/Functor/OfSequence.lean

Statistics

Metric	Count
Definitions `map`, `ofOpSequence`, `ofSequence`, `ofOpSequence`, `ofSequence`	5
Theorems `congr_f`, `map_comp`, `map_comp_assoc`, `map_id`, `map_le_succ`, `ofOpSequence_map_homOfLE_succ`, `ofOpSequence_obj`, `ofSequence_map_homOfLE_succ`, `ofSequence_obj`, `ofOpSequence_app`, `ofSequence_app`	11
Total	16

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`ofOpSequence` 📖	CompOp	10 math math: `CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_pos_assoc`, `CategoryTheory.Limits.SequentialProduct.functorMap_commSq_aux`, `CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_neg_assoc`, `ofOpSequence_obj`, `ofOpSequence_map_homOfLE_succ`, `CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_pos`, `CategoryTheory.Limits.SequentialProduct.cone_π_app`, `CategoryTheory.Limits.SequentialProduct.functorMap_commSq_succ`, `CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_neg`, `CategoryTheory.Limits.SequentialProduct.functorMap_commSq`
`ofSequence` 📖	CompOp	2 math math: `ofSequence_map_homOfLE_succ`, `ofSequence_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofOpSequence_map_homOfLE_succ` 📖	mathematical	—	`map` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `Nat.instPreorder` `ofOpSequence` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.homOfLE`	—	`ofSequence_map_homOfLE_succ`
`ofOpSequence_obj` 📖	mathematical	—	`obj` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `Nat.instPreorder` `ofOpSequence` `Opposite.unop`	—	—
`ofSequence_map_homOfLE_succ` 📖	mathematical	—	`map` `Preorder.smallCategory` `Nat.instPreorder` `ofSequence` `CategoryTheory.homOfLE`	—	`OfSequence.map_le_succ`
`ofSequence_obj` 📖	mathematical	—	`obj` `Preorder.smallCategory` `Nat.instPreorder` `ofSequence`	—	—

CategoryTheory.Functor.OfSequence

Definitions

Name	Category	Theorems
`map` 📖	CompOp	4 math math: `map_le_succ`, `map_comp_assoc`, `map_comp`, `map_id`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_f` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.eqToHom`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`map_comp` 📖	mathematical	—	`map` `LE.le.trans` `Nat.instPreorder` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`LE.le.trans` `map_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id` `map.eq_3` `CategoryTheory.Category.assoc`
`map_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `map` `LE.le.trans` `Nat.instPreorder`	—	`LE.le.trans` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_comp`
`map_id` 📖	mathematical	—	`map` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`map_le_succ` 📖	mathematical	—	`map`	—	—

CategoryTheory.NatTrans

Definitions

Name	Category	Theorems
`ofOpSequence` 📖	CompOp	1 math math: `ofOpSequence_app`
`ofSequence` 📖	CompOp	1 math math: `ofSequence_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofOpSequence_app` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `Nat.instPreorder` `Opposite.op` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.homOfLE`	`app` `ofOpSequence` `Opposite.unop`	—	—
`ofSequence_app` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `Nat.instPreorder` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE`	`app` `ofSequence`	—	—

---

← Back to Index