prod_unique — Mathlib

English

For a monoid hom f: M →* N × P, the pair of projections recovers f: ((fst).comp f).prod ((snd).comp f) = f.

Русский

Для моноидного гомоморфизма f: M →* N × P пара проекций восстанавливает f: ((fst).comp f).prod ((snd).comp f) = f.

LaTeX

$$$ ((\\operatorname{fst}_{N P} \\circ f).\\text{prod} (\\operatorname{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]

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