comp_apply

Mathlib.Algebra.Category.Semigrp.Basic

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

English

Let f: M → N and g: N → T be morphisms. For every x ∈ M, (f ≫ g) x = g (f x).

Русский

Пусть f: M → N и g: N → T — морфизмы. Для каждого x ∈ M верно (f ≫ g) x = g (f x).

LaTeX

$$$\\forall {M N T}, (f: M \\to N), (g: N \\to T), \\forall x: M, (f \\gg g) x = g (f x)$$$

Lean4

@[to_additive]
theorem comp_apply {M N T : MagmaCat} (f : M ⟶ N) (g : N ⟶ T) (x : M) : (f ≫ g) x = g (f x) := by simp

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

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

Разделы

Аффилиация

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