comp_apply — Mathlib

English

Let M,N,T be commutative monoids and f: M → N, g: N → T be morphisms. Then the composite g ∘ f acts pointwise: for every x ∈ M, (g ∘ f)(x) = g(f(x)).

Русский

Пусть M, N и T — коммутативные моноиды, а f: M → N и g: N → T — морфизмы. Тогда композиция g ∘ f действует по точкам: для каждого x ∈ M выполняется (g ∘ f)(x) = g(f(x)).

LaTeX

$$$\forall f: M \to N,\; \forall g: N \to T,\; \forall x \in M:\quad (g \circ f)(x) = g(f(x)).$$$

Lean4

@[to_additive]
theorem comp_apply {M N T : CommMonCat} (f : M ⟶ N) (g : N ⟶ T) (x : M) : (f ≫ g) x = g (f x) := by simp

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