Def CategoryTheory.Over.CreatesConnected.natTransInOver

Modification history

2025-09-30 18:42

Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean

chore(CategoryTheory/Limits): generalise from `Over` to `CostructuredArrow` (#30074) …

Deleted CategoryTheory.Over.CreatesConnected.natTransInOver View on Github →

2023-03-13 12:32

Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean

feat: port CategoryTheory.Limits.Constructions.Over.Connected (#2831)

Added CategoryTheory.Over.CreatesConnected.natTransInOver View on Github →