prod_ext — Mathlib

English

The map producing the product map from a pair of maps is a linear equivalence, and its inverse is obtained by composing with the projections inl and inr.

Русский

Отображение, выдающее произведение из пары отображений, является линейной эквивелентностью; обратное строится через композицию с вложениями inl и inr.

LaTeX

$$$$ \text{prodEquiv} : ((M \to_L M_2) \times (M \to_L M_3)) \simeq_L (M \to_L (M_2 \times M_3)) $$$$

Lean4

@[ext]
theorem prod_ext {f g : M × M₂ →L[R] M₃} (hl : f.comp (inl _ _ _) = g.comp (inl _ _ _))
    (hr : f.comp (inr _ _ _) = g.comp (inr _ _ _)) : f = g :=
  prod_ext_iff.2 ⟨hl, hr⟩

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