Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.limits.lim_lax_map

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_map View on Github →