comp_apply

Mathlib.Algebra.Category.Grp.Basic

URI: https://scilib.ai/kg/mathlib#GrpCat.comp_apply

English

The value of the composite morphism on an element x is the result of applying f and then g.

Русский

Значение композиции морфизма на элементе x равно применению сначала f, затем g.

LaTeX

$$$ (f \gg g)\, x = g\,(f\,x). $$$

Lean4

@[to_additive]
theorem comp_apply {X Y T : GrpCat} (f : X ⟶ Y) (g : Y ⟶ T) (x : X) : (f ≫ g) x = g (f x) := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru