coprod_unique — Mathlib

English

For any monoid homomorphism f: M × N →* P, the identity (f ∘ (inl M N)) ⊔ (f ∘ (inr M N)) = f holds, i.e., a map is determined by its restrictions to M and N.

Русский

Для любого моноид-гомоморфизма f: M × N →* P верно равенство (f ∘ inl M N) ⊔ (f ∘ inr M N) = f, то есть отображение определяется его ограничения на M и N.

LaTeX

$$$f:\\,M\\times N \\to^* P \quad \\Rightarrow \\quad (f \\circ \\mathrm{inl}_{M,N}) \\coprod (f \\circ \\mathrm{inr}_{M,N}) = f.$$$

Lean4

@[to_additive (attr := simp)]
theorem coprod_unique (f : M × N →* P) : (f.comp (inl M N)).coprod (f.comp (inr M N)) = f :=
  ext fun x => by simp [coprod_apply, inl_apply, inr_apply, ← map_mul]

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