Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-12 17:00 817c70db

View on Github →

feat(category_theory/*): Functors about comma categories. (#9627) Added pre and post for comma, structured_arrow, costructured_arrow.

Estimated changes

Modified src/category_theory/comma.lean

added def category_theory.comma.post

added def category_theory.comma.pre_left

added def category_theory.comma.pre_right

Modified src/category_theory/structured_arrow.lean

added def category_theory.costructured_arrow.post

added def category_theory.costructured_arrow.pre

added def category_theory.structured_arrow.post

added def category_theory.structured_arrow.pre