mathlib3 documentation

category_theory.concrete_category.reflects_isomorphisms

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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