PEmpty

📁 Source: Mathlib/CategoryTheory/PEmpty.lean

Statistics

Metric	Count
Definitions empty, emptyExt, isEmptyExt, uniqueFromEmpty, emptyEquivalence, equivalenceOfIsEmpty, functorOfIsEmpty	7
Theorems empty_ext', instIsEmptyDiscrete	2
Total	9

CategoryTheory

Definitions

Name	Category	Theorems
emptyEquivalence 📖	CompOp	—
equivalenceOfIsEmpty 📖	CompOp	—
functorOfIsEmpty 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsEmptyDiscrete 📖	mathematical	—	IsEmpty Discrete	—	Function.isEmpty

CategoryTheory.Functor

Definitions

Name	Category	Theorems
empty 📖	CompOp	28 math math: CategoryTheory.Limits.BinaryFan.rightUnitor_hom, CategoryTheory.Limits.asEmptyCocone_pt, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_isTerminalTensorUnit_lift_hom, CategoryTheory.Over.preservesTerminalIso_pullback, CategoryTheory.Limits.asEmptyCone_pt, CategoryTheory.Limits.PreservesTerminal.of_iso_comparison, CategoryTheory.IsInitial.isVanKampenColimit, CategoryTheory.Limits.BinaryFan.rightUnitor_inv, CategoryTheory.Presieve.preservesTerminal_of_isSheaf_for_empty, SSet.hoFunctor.preservesTerminal, CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.leftUnitor_naturality, CategoryTheory.Limits.preservesInitial_of_isIso, CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.triangle, CategoryTheory.Limits.preservesTerminal_of_iso, CategoryTheory.Limits.asEmptyCocone_ι_app, preservesInitialObject_of_preservesZeroMorphisms, CategoryTheory.Limits.asEmptyCone_π_app, Monoidal.ε_of_cartesianMonoidalCategory, CategoryTheory.Limits.BinaryFan.leftUnitor_hom, CategoryTheory.Limits.PreservesInitial.of_iso_comparison, preservesTerminalObject_of_preservesZeroMorphisms, CategoryTheory.IsSifted.colim_preservesTerminal_of_isSifted, CategoryTheory.Limits.BinaryFan.leftUnitor_inv, CategoryTheory.Limits.preservesTerminal_of_isIso, CategoryTheory.CartesianMonoidalCategory.preservesLimit_empty_of_isIso_terminalComparison, CategoryTheory.Limits.preservesInitial_of_iso, CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso_id, CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.rightUnitor_naturality
emptyExt 📖	CompOp	—
isEmptyExt 📖	CompOp	—
uniqueFromEmpty 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
empty_ext' 📖	—	—	—	—	ext

---

← Back to Index