fst_prod — Mathlib

English

There is a natural equivalence between pairs of morphisms (f:A→ₙₐ[R] B, g:A→ₙₐ[R] C) and a single morphism A→ₙₐ[R] B×C, given by f,g ↦ f.prod g with inverse given by h ↦ (fst ∘ h, snd ∘ h).

Русский

Существует естественное эквивалентное соответствие между парами морфизмов (f: A→ₙₐ[R] B, g: A→ₙₐ[R] C) и одним морфизмом A→ₙₐ[R] B×C, заданное преобразованием f,g ↦ f.prod g и обратным преобразованием h ↦ (fst ∘ h, snd ∘ h).

LaTeX

$$$(A \to_{R} B) \times (A \to_{R} C) \simeq (A \to_{R} (B \times C))$ with toFun((f,g))=f.prod g and invFun(h)=(\text{fst} \circ h, \text{snd} \circ h).$$$

Lean4

@[simp]
theorem fst_prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : (fst R B C).comp (prod f g) = f := by rfl

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