mathlib documentation

category_theory.concrete_category.reflects_isomorphisms

A forget₂ C D forgetful functor between concrete categories C and D whose forgetful functors both reflect isomorphisms, itself reflects isomorphisms.

source
@[instance]
def category_theory.forget.reflects_isomorphisms  :
category_theory.reflects_isomorphisms (category_theory.forget (Type u))
source
theorem category_theory.reflects_isomorphisms_forget₂ (C : Type (u+1)) [category_theory.category C] [category_theory.concrete_category C] (D : Type (u+1)) [category_theory.category D] [category_theory.concrete_category D] [category_theory.has_forget₂ C D] [category_theory.reflects_isomorphisms (category_theory.forget C)] :
category_theory.reflects_isomorphisms (category_theory.forget₂ C D)

A forget₂ C D forgetful functor between concrete categories C and D where forget C reflects isomorphisms, itself reflects isomorphisms.