Final

📁 Source: Mathlib/CategoryTheory/Join/Final.lean

Statistics

Metric	Count
Definitions costructuredArrowEquiv, structuredArrowEquiv	2
Theorems instFinalInclRightOfIsConnected, instInitialInclLeftOfIsConnected	2
Total	4

CategoryTheory.Join

Definitions

Name	Category	Theorems
costructuredArrowEquiv 📖	CompOp	—
structuredArrowEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFinalInclRightOfIsConnected 📖	mathematical	—	CategoryTheory.Functor.Final CategoryTheory.Join instCategory inclRight	—	CategoryTheory.isConnected_of_equivalent CategoryTheory.isConnected_of_isInitial inclRightFull inclRightFaithful
instInitialInclLeftOfIsConnected 📖	mathematical	—	CategoryTheory.Functor.Initial CategoryTheory.Join instCategory inclLeft	—	CategoryTheory.isConnected_of_isTerminal inclLeftFull inclLeftFaithful CategoryTheory.isConnected_of_equivalent

---

← Back to Index