comp_apply — Mathlib

English

The value of the composition at a is the value of the outer morphism at the image of a under the inner morphism: (comp f g) a = f(g(a)).

Русский

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

LaTeX

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

Lean4

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

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