prod_unique — Mathlib

English

The product map from M to M' and N to N' is uniquely determined by its projections fst and snd; i.e., the pair of composed maps recovers f.

Русский

Произведение двух гомоморфизмов полностью определяет гомоморфизм в произведении, восстанавливая его по проекциям fst и snd.

LaTeX

$$$((\mathrm{fst}_{N,P} \circ f) ).prod ((\mathrm{snd}_{N,P} \circ f)) = f$$$

Lean4

@[to_additive (attr := simp) prod_unique]
theorem prod_unique (f : M →ₙ* N × P) : ((fst N P).comp f).prod ((snd N P).comp f) = f :=
  ext fun x => by simp only [prod_apply, coe_fst, coe_snd, comp_apply]

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