noncommCoprod_comp_inl — Mathlib

English

The coproduct composed with the left injection equals f, and with the right injection equals g.

Русский

Копродукт после вставки слева (inl) даёт f, после вставки справа (inr) даёт g.

LaTeX

$$$ (f.noncommCoprod g comm).\\mathrm{comp}(\\mathrm{inl} M N) = f \\quad\\text{and}\\quad (f.noncommCoprod g comm).\\mathrm{comp}(\\mathrm{inr} M N) = g. $$$

Lean4

@[to_additive (attr := simp)]
theorem noncommCoprod_comp_inl : (f.noncommCoprod g comm).comp (inl M N) = f :=
  ext fun x => by simp

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