Def CategoryTheory.ConnectedComponents.liftFunctor

Modification history

2025-12-13 14:21
Mathlib/CategoryTheory/ConnectedComponents.lean
chore: use `Category*` everywhere (#32842) …
Modified CategoryTheory.ConnectedComponents.liftFunctorView on Github →
2025-04-30 12:59
Mathlib/CategoryTheory/ConnectedComponents.lean
style: further whitespace fixes (#24467) …
Modified CategoryTheory.ConnectedComponents.liftFunctorView on Github →
2024-08-30 08:52
Mathlib/CategoryTheory/ConnectedComponents.lean
style: some formatting fixes (#16263) …
Modified CategoryTheory.ConnectedComponents.liftFunctorView on Github →
2024-08-12 22:49
Mathlib/CategoryTheory/ConnectedComponents.lean
feat(CategoryTheory/Adjunction): `typeToCat` is right adjoint to `connectedComponents` functor (#15614) …
Added CategoryTheory.ConnectedComponents.liftFunctorView on Github →