comp_apply

Mathlib.Order.Category.NonemptyFinLinOrd

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

English

For f: X → Y and g: Y → Z in NonemptyFinLinOrd, (f ≫ g)(x) = g(f(x)).

Русский

Для морфизмов f: X → Y и g: Y → Z в NonemptyFinLinOrd выполняется (f ≫ g)(x) = g(f(x)).

LaTeX

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

Lean4

theorem comp_apply {X Y Z : NonemptyFinLinOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp

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

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

Разделы

Аффилиация

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