Connected

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

Name	Kind	Assumes	Proves	Validates	Depends On
`final_fst` 📖	mathematical	—	`Functor.Final` `prod'` `Prod.fst`	—	—
`final_snd` 📖	mathematical	—	`Functor.Final` `prod'` `Prod.snd`	—	—
`initial_fst` 📖	mathematical	—	`Functor.Initial` `prod'` `Prod.fst`	—	—
`initial_snd` 📖	mathematical	—	`Functor.Initial` `prod'` `Prod.snd`	—	—
`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`

---