Theorems · Theorem · category theory

CategoryTheory.StrongMono.of_arrow_iso

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B A' B' : C} {f : B ⟶ A} {g : B' ⟶ A'}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g) [h : CategoryTheory.StrongMono f],
  CategoryTheory.StrongMono g

Defined in

Mathlib.CategoryTheory.Limits.Shapes.StrongEpi

Cited by

1 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.StrongMono