prod_unique — Mathlib

English

For maps f: T → R and g: T → S, the composed product maps satisfy (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g).

Русский

Для отображений f: T → R и g: T → S выполнено равенство (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g).

LaTeX

$$$ (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g). $$$

Lean4

theorem prod_unique (f : R →ₙ+* S × T) : ((fst S T).comp f).prod ((snd S T).comp f) = f :=
  ext fun x => by simp only [prod_apply, coe_fst, coe_snd, comp_apply]

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