comp_apply

Mathlib.Algebra.Category.CommBialgCat

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

English

For any morphisms f:A→B and g:B→C, and any a∈A, (f ≫ g)(a) = g(f(a)).

Русский

Для морфизмов f:A→B и g:B→C и элемента a∈A выполняется (f ≫ g)(a) = g(f(a)).

LaTeX

$$$\forall f:A\to B\, g:B\to C\, a\in A,\ (f\gg 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