coprodComparison_inr — Mathlib

English

For any F with binary coproducts, coprod.inr ≫ coprodComparison F A B = F.map coprod.inr.

Русский

Для любого F с бинарными копродуктами: coprod.inr ≫ coprodComparison F A B = F.map coprod.inr.

LaTeX

$$$ \\operatorname{coprod.inr} \\circ \\operatorname{coprodComparison} F A B = F(\\operatorname{coprod.inr}) $$$

Lean4

@[reassoc (attr := simp)]
theorem coprodComparison_inr : coprod.inr ≫ coprodComparison F A B = F.map coprod.inr :=
  coprod.inr_desc _ _

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