preimage_comp — Mathlib

English

The preimage operation preserves composition: the preimage of a composition is the composition of preimages.

Русский

Отражение предобраза сохраняет композицию: предобраз композиции равен композиции предобразов.

LaTeX

$$$\forall f,g:\; hF.preimage(f \circ g) = hF.preimage(f) \circ hF.preimage(g)$$$

Lean4

@[simp, reassoc]
theorem preimage_comp {X Y Z : C} (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z) :
    hF.preimage (f ≫ g) = hF.preimage f ≫ hF.preimage g :=
  hF.map_injective (by simp)

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