CategoryTheory.MorphismProperty.IsInvertedBy.of_comp

theorem CategoryTheory.MorphismProperty.IsInvertedBy.of_comp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{u_4, u_1} C₁] [inst_1 : CategoryTheory.Category.{u_5, u_2} C₂] [inst_2 : CategoryTheory.Category.{u_6, u_3} C₃] (W : CategoryTheory.MorphismProperty C₁) (F : CategoryTheory.Functor C₁ C₂), W.IsInvertedBy F → ∀ (G : CategoryTheory.Functor C₂ C₃), W.IsInvertedBy (F.comp G)

The theorem `CategoryTheory.MorphismProperty.IsInvertedBy.of_comp` states that for any two categories `C₁`, `C₂`, and `C₃`, given a `MorphismProperty` `W` in the category `C₁` and a functor `F` from `C₁` to `C₂` which maps all morphisms in `W` to isomorphisms in `C₂`, then for any functor `G` from `C₂` to `C₃`, the composition of the functors `F` and `G` will also map all morphisms in `W` to isomorphisms in `C₃`. This theorem hence ensures that the property of mapping morphisms to isomorphisms is preserved under the composition of functors.

More concisely: If functors F from C₁ to C₂ and G from C₂ to C₃ preserve a property W of morphisms in C₁, i.e., map all morphisms in W to isomorphisms in their respective categories, then the composition of F and G preserves W, mapping all morphisms in W to isomorphisms in C₃.