comp_apply

Mathlib.Algebra.Category.CommAlgCat.Basic

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

English

The composition of two morphisms f: A ⟶ B and g: B ⟶ C acts as usual: (f ≫ g) applied to a equals g(f(a)).

Русский

Сложение морфизмов f: A → B и g: B → C действует обычным образом: (f ≫ g)(a) = g(f(a)).

LaTeX

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

Lean4

theorem comp_apply (f : A ⟶ B) (g : B ⟶ C) (a : A) : (f ≫ g) a = g (f a) := by simp

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

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

Разделы

Аффилиация

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