inl — Mathlib

English

The two projections compose with the product to recover the original morphisms, etc.

Русский

Две проекции составляются с произведением и восстанавливают исходные морфизмы и т.д.

LaTeX

$$$(\text{fst} \circ (f \mathrm{.prod} g))=f$ and $(\text{snd} \circ (f \mathrm{.prod} g))=g$$$

Lean4

/-- The left injection into a product is a non-unital algebra homomorphism. -/
def inl : A →ₙₐ[R] A × B :=
  prod 1 0

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