inl_comp_pushoutComparison — Mathlib

English

The pushout injection composed with pushoutComparison equals the functorial image of the pushout.inl.

Русский

Инъекция пушаута, умноженная на pushoutComparison, равна образу pushout.inl через F.

LaTeX

$$$\mathrm{pushout.inl} \; f g \; ≫ \mathrm{pushoutComparison} G f g = G\,\mathrm{map}(\mathrm{pushout.inl} f g)$$$

Lean4

@[reassoc (attr := simp)]
theorem inl_comp_pushoutComparison (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] [HasPushout (G.map f) (G.map g)] :
    pushout.inl _ _ ≫ pushoutComparison G f g = G.map (pushout.inl _ _) :=
  pushout.inl_desc _ _ _

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