inr_desc — Mathlib

English

Let X ⊔ Y be a binary coproduct with injections i1: X → X ⊔ Y and i2: Y → X ⊔ Y, and a morphism f: X → W, g: Y → W. Then i2 followed by the universal desc to W equals g, i.e., i2 ≫ desc f g = g.

Русский

Пусть X ⊔ Y — бинарный coproduct с внедрениями i1: X → X ⊔ Y и i2: Y → X ⊔ Y, а также f: X → W, g: Y → W. Тогда i2 ∘ desc(f,g) = g.

LaTeX

$$$\\mathrm{coprod.inr} \\circ \\mathrm{coprod.desc}(f,g) = g$$$

Lean4

@[reassoc]
theorem inr_desc {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : coprod.inr ≫ coprod.desc f g = g :=
  colimit.ι_desc _ _

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