def IsConservative {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Prop

A functor F is conservative if it reflects isomorphisms: whenever F.map g is an isomorphism, so is g.

theorem isConservative_iff_reflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : IsConservative F ↔ F.ReflectsIsomorphisms

The plain Prop notion IsConservative agrees with the type-class ReflectsIsomorphisms from mathlib.