comp_apply — Mathlib

English

Applying the composite to an input yields applying the first to the result of the second.

Русский

Применение композиции к аргументу даёт сначала применить вторую функцию к аргументу, затем первую к полученному значению.

LaTeX

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

Lean4

theorem comp_apply (f : B →ₛₙₐ[ψ] C) (g : A →ₛₙₐ[φ] B) [MonoidHom.CompTriple φ ψ χ] (x : A) : f.comp g x = f (g x) :=
  rfl

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