comp_apply — Mathlib

English

The value of the composed map at a equals applying the outer map to the inner value: (comp f g) a = f (g a).

Русский

Значение композиции в точке a равно применению внешнего гомоморфизма к значению внутреннего: (comp f g) a = f (g a).

LaTeX

$$$\mathrm{comp}(f,g)(a) = f(g(a))$$$

Lean4

@[simp]
theorem comp_apply (f : B →⋆ₙₐ[R] C) (g : A →⋆ₙₐ[R] B) (a : A) : comp f g a = f (g a) :=
  rfl

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