lift_apply_inr — Mathlib

English

Let M,N be monoids and P a monoid. For any monoid homomorphisms f: M →* P and g: N →* P, the universal map lift f g: M ∗ N →* P satisfies (lift f g)(inr x) = g x for all x ∈ N.

Русский

Пусть M, N — моноиды, P — моноид. Для любых мороморфизмов f: M →* P и g: N →* P обобщённое отображение lift f g: M ∗ N →* P удовлетворяет (lift f g)(inr x) = g x для всех x ∈ N.

LaTeX

$$$\\\\forall f:M \\\\to^* P\\\\, \\\\forall g:N \\\\to^* P\\\\, \\\\forall x\\\\in N,\quad (\\\\mathrm{lift} \\, f \\, g)(\\\\mathrm{inr} \\, x) = g \\, x.$$$

Lean4

@[to_additive (attr := simp)]
theorem lift_apply_inr (f : M →* P) (g : N →* P) (x : N) : lift f g (inr x) = g x :=
  rfl

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