Commit 2023-03-13 12:32 cedb8751

View on Github →

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

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Over.CreatesConnected.natTransInOver

added def CategoryTheory.Over.CreatesConnected.raiseCone

added def CategoryTheory.Over.CreatesConnected.raisedConeIsLimit

added theorem CategoryTheory.Over.CreatesConnected.raised_cone_lowers_to_original