Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-16 04:46 b1e7fb2d

View on Github →

feat (category_theory/over): composition of over.map (#3798) Filtering in some defs from the topos project. ~~Depends on #3797.~~

Estimated changes

Modified src/category_theory/over.lean

added def category_theory.over.map_comp

added def category_theory.over.map_id

added def category_theory.under.map_comp

added def category_theory.under.map_id