Commit 2023-06-10 20:32 da6373c6

View on Github →

feat: port CategoryTheory.Monoidal.Limits (#4956)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Limits.lean

added def CategoryTheory.Limits.limLax

added theorem CategoryTheory.Limits.limLax_map

added theorem CategoryTheory.Limits.limLax_obj'

added theorem CategoryTheory.Limits.limLax_obj

added theorem CategoryTheory.Limits.limLax_ε

added theorem CategoryTheory.Limits.limLax_μ

added theorem CategoryTheory.Limits.limitFunctorial_map