comp_apply — Mathlib

English

Applying the composed map to an argument yields the same as applying the outer map to the inner map’s result.

Русский

Применение композиции к аргументу даёт результат как от применения внешней функции к результату внутренней.

LaTeX

$$$ f\circ g (a) = f(g(a)) $$$

Lean4

@[simp]
theorem comp_apply (f : β →+*o γ) (g : α →+*o β) (a : α) : f.comp g a = f (g a) :=
  rfl

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