of_apply — Mathlib

English

Two monoid homomorphisms from CoprodI M to N are equal if they agree on all inclusions of summands M_i → CoprodI M; this is the extensionality principle for CoprodI.

Русский

Два моноид-гомоморфизма из CoprodI M в N равны, если они согласны на все включения M_i в CoprodI M; это экстензионность CoprodI.

LaTeX

$$$\\forall i,\\; f \\circ \\mathrm{of}_i = g \\circ \\mathrm{of}_i \\Rightarrow f = g$.$$

Lean4

theorem of_apply {i} (m : M i) : of m = Con.mk' _ (FreeMonoid.of <| Sigma.mk i m) :=
  rfl

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