coprodComparison_inl — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem coprodComparison_inl : coprod.inl ≫ coprodComparison F A B = F.map coprod.inl :=
  coprod.inl_desc _ _

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