products): if each `f b ⟶ g b` is mono, then `∏ f ⟶ ∏ g` is mono (#16180)

Commit

3 years ago

feat(category_theory/limits/shapes/products): if each `f b ⟶ g b` is mono, then `∏ f ⟶ ∏ g` is mono (#16180) and its dual version: if each `f b ⟶ g b` is epi, then `∐ f ⟶ ∐ g` is epi

Author

jjaassoonn

Parents

f0c55c2a

mathlib e11bafa5 - feat(category_theory/limits/shapes/products): if each `f b ⟶ g b` is mono, then `∏ f ⟶ ∏ g` is mono (#16180)

mathlib
e11bafa5 - feat(category_theory/limits/shapes/products): if each `f b ⟶ g b` is mono, then `∏ f ⟶ ∏ g` is mono (#16180)