CategoryTheory.reflectsIsomorphisms_forget₂

theorem CategoryTheory.reflectsIsomorphisms_forget₂ : ∀ (C : Type (u + 1)) [inst : CategoryTheory.Category.{u_1, u + 1} C] [inst_1 : CategoryTheory.ConcreteCategory C] (D : Type (u + 1)) [inst_2 : CategoryTheory.Category.{u_2, u + 1} D] [inst_3 : CategoryTheory.ConcreteCategory D] [inst_4 : CategoryTheory.HasForget₂ C D] [inst_5 : (CategoryTheory.forget C).ReflectsIsomorphisms], (CategoryTheory.forget₂ C D).ReflectsIsomorphisms

The theorem `CategoryTheory.reflectsIsomorphisms_forget₂` states that for any two concrete categories `C` and `D`, if the forgetful functor `forget C` from `C` to `Type` reflects isomorphisms, then the forgetful functor `forget₂ C D` from `C` to `D` also reflects isomorphisms. In other words, if an isomorphism in the category `C` remains an isomorphism when we forget the additional structure and consider it as an object in `Type`, then it also remains an isomorphism when we forget some structure and consider it as an object in `D`.

More concisely: If `forget C` reflects isomorphisms in `Type`, then `forget₂ C D` also reflects isomorphisms in `D`.