Documentation Verification Report

Push

📁 Source: Mathlib/Combinatorics/Quiver/Push.lean

Statistics

Metric	Count
Definitions `Push`, `of`, `PushQuiver`, `instPush`	4
Theorems `lift_comp`, `lift_obj`, `lift_unique`, `of_obj`, `instNonemptyPush`	5
Total	9

Quiver

Definitions

Name	Category	Theorems
`Push` 📖	CompOp	6 math math: `instNonemptyPush`, `Push.of_obj`, `Push.lift_comp`, `Push.of_reverse`, `Push.lift_obj`, `Push.ofMapReverse`
`PushQuiver` 📖	CompData	—
`instPush` 📖	CompOp	5 math math: `Push.of_obj`, `Push.lift_comp`, `Push.of_reverse`, `Push.lift_obj`, `Push.ofMapReverse`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNonemptyPush` 📖	mathematical	—	`Push`	—	—

Quiver.Push

Definitions

Name	Category	Theorems
`of` 📖	CompOp	4 math math: `of_obj`, `lift_comp`, `of_reverse`, `ofMapReverse`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lift_comp` 📖	mathematical	`Prefunctor.obj`	`Prefunctor.comp` `Quiver.Push` `Quiver.instPush` `of` `lift`	—	`Prefunctor.ext`
`lift_obj` 📖	mathematical	`Prefunctor.obj`	`Quiver.Push` `Quiver.instPush` `lift`	—	—
`lift_unique` 📖	mathematical	`Prefunctor.obj` `Quiver.Push` `Quiver.instPush` `Prefunctor.comp` `of`	`lift`	—	`Prefunctor.ext`
`of_obj` 📖	mathematical	—	`Prefunctor.obj` `Quiver.Push` `Quiver.instPush` `of`	—	—

---

← Back to Index