English
If P is closed under subobjects in C and F: D ⥤ C preserves monomorphisms, then the inverse image property (P.invereseImage F) is closed under subobjects in D.
Русский
Если P замкнуто по подобъектам в C и F: D ⥤ C сохраняет мономорфизмы, то обратное изображение P^{-1}F по отношению к D замкнуто по подобъектам.
LaTeX
$$$\forall F:D\to C\ [F.\PreservesMonomorphisms]\; (P^{ -1}F).\IsClosedUnderSubobjects$$$
Lean4
instance (F : D ⥤ C) [F.PreservesMonomorphisms] : (P.inverseImage F).IsClosedUnderSubobjects where
prop_of_mono f _ h := P.prop_of_mono (F.map f) h
