Connected

📁 Source: Mathlib/CategoryTheory/Limits/Final/Connected.lean

Statistics

Metric	Count
Definitions	0
Theorems final_fst, final_snd, initial_fst, initial_snd, instFinalDiscreteOfIsConnected, instInitialDiscreteOfIsConnected, isConnected_iff_final_of_unique, isConnected_iff_initial_of_unique	8
Total	8

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
final_fst 📖	mathematical	—	Functor.Final prod' Prod.fst	—	Functor.final_comp instFinalProdProd Functor.final_of_isRightAdjoint Functor.isRightAdjoint_of_isEquivalence Functor.isEquivalence_refl instFinalDiscreteOfIsConnected Equivalence.isEquivalence_functor
final_snd 📖	mathematical	—	Functor.Final prod' Prod.snd	—	Functor.final_comp Functor.final_of_isRightAdjoint Functor.isRightAdjoint_of_isEquivalence Equivalence.isEquivalence_functor final_fst
initial_fst 📖	mathematical	—	Functor.Initial prod' Prod.fst	—	Functor.initial_comp instInitialProdProd Functor.initial_of_isLeftAdjoint Functor.isLeftAdjoint_of_isEquivalence Functor.isEquivalence_refl instInitialDiscreteOfIsConnected Equivalence.isEquivalence_functor
initial_snd 📖	mathematical	—	Functor.Initial prod' Prod.snd	—	Functor.initial_comp Functor.initial_of_isLeftAdjoint Functor.isLeftAdjoint_of_isEquivalence Equivalence.isEquivalence_functor initial_fst
instFinalDiscreteOfIsConnected 📖	mathematical	—	Functor.Final Discrete discreteCategory	—	isConnected_iff_final_of_unique
instInitialDiscreteOfIsConnected 📖	mathematical	—	Functor.Initial Discrete discreteCategory	—	isConnected_iff_initial_of_unique
isConnected_iff_final_of_unique 📖	mathematical	—	IsConnected Functor.Final Discrete discreteCategory	—	isConnected_iff_of_equivalence Unique.instSubsingleton Functor.Final.out
isConnected_iff_initial_of_unique 📖	mathematical	—	IsConnected Functor.Initial Discrete discreteCategory	—	isConnected_iff_of_equivalence Unique.instSubsingleton Functor.Initial.out

---

← Back to Index