Commit 2023-04-25 09:36 6137962d

View on Github →

feat: port CategoryTheory.Limits.Constructions.WeaklyInitial (#3627)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Constructions/WeaklyInitial.lean

added theorem CategoryTheory.hasInitial_of_weakly_initial_and_hasWideEqualizers

added theorem CategoryTheory.has_weakly_initial_of_weakly_initial_set_and_hasProducts