prodEquiv — Mathlib

English

The two directions in prodEquiv are mutually inverse, establishing a natural equivalence between pairs of morphisms and product morphisms.

Русский

Два направления в prodEquiv взаимно обратны, устанавливая естественную эквивалентность между парами морфизмов и произведением морфизмов.

LaTeX

$$$\text{toFun}$ and $\text{invFun}$ form an equivalence between the structures.$$

Lean4

/-- Taking the product of two maps with the same domain is equivalent to taking the product of
their codomains. -/
@[simps]
def prodEquiv : (A →ₙₐ[R] B) × (A →ₙₐ[R] C) ≃ (A →ₙₐ[R] B × C)
    where
  toFun f := f.1.prod f.2
  invFun f := ((fst _ _ _).comp f, (snd _ _ _).comp f)

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