ToApp
📁 Source: Mathlib/Tactic/CategoryTheory/ToApp.lean
Statistics
| Metric | Count |
|---|---|
| 6 | |
TheoremstoNatTrans_congr | 1 |
| Total | 7 |
Mathlib.Tactic.CategoryTheory.ToApp
Definitions
| Name | Category | Theorems |
|---|---|---|
catAppSimp 📖 | CompOp | — |
toAppExpr 📖 | CompOp | — |
toCatExpr 📖 | CompOp | — |
toNatTransExpr 📖 | CompOp | — |
to_app 📖 | CompOp | — |
«termTo_app_of%_» 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
toNatTrans_congr 📖 | mathematical | — | CategoryTheory.Cat.Hom₂.toNatTrans | — | — |
---