Mathlib v3 is deprecated. Go to Mathlib v4

Def category_theory.limits.lim_lax

Modification history

2020-09-19 04:51

src/category_theory/monoidal/limits.lean

feat(category_theory): `lim : (J ⥤ C) ⥤ C` is lax monoidal when `C` is monoidal (#4132) …

Added category_theory.limits.lim_lax View on Github →