inverseImage — Mathlib

English

If P contains identities and F: C ⥤ D, then (P.inverseImage F).ContainsIdentities.

Русский

Если P содержит идентичности и F: C ⥤ D, то (P.inverseImage F) содержит идентичности.

LaTeX

$$$(P.inverseImage F).ContainsIdentities$$$

Lean4

instance inverseImage {P : MorphismProperty D} [P.ContainsIdentities] (F : C ⥤ D) :
    (P.inverseImage F).ContainsIdentities where id_mem X := by simpa only [← F.map_id] using P.id_mem (F.obj X)

Похожие утверждения