Basic

📁 Source: Mathlib/CategoryTheory/MarkovCategory/Basic.lean

Statistics

Metric	Count
Definitions isTerminalUnit, toCopyDiscardCategory	2
Theorems discard_natural, discard_natural_assoc, eq_discard, instSubsingletonHomTensorUnit	4
Total	6

CategoryTheory.MarkovCategory

Definitions

Name	Category	Theorems
isTerminalUnit 📖	CompOp	—
toCopyDiscardCategory 📖	CompOp	3 math math: eq_discard, discard_natural, discard_natural_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discard_natural 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.counit CategoryTheory.CopyDiscardCategory.comonObj toCopyDiscardCategory	—	—
discard_natural_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.counit CategoryTheory.CopyDiscardCategory.comonObj toCopyDiscardCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' discard_natural
eq_discard 📖	mathematical	—	CategoryTheory.ComonObj.counit CategoryTheory.CopyDiscardCategory.comonObj toCopyDiscardCategory	—	CategoryTheory.Category.comp_id CategoryTheory.CopyDiscardCategory.discard_unit discard_natural
instSubsingletonHomTensorUnit 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	CategoryTheory.Limits.IsTerminal.hom_ext

---

← Back to Index