comp_apply

Mathlib.Order.Category.DistLat

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

English

In DistLat, the composition of two morphisms f: X → Y and g: Y → Z satisfies (g ∘ f)(x) = g(f(x)) for all x ∈ X.

Русский

В DistLat композиция морфизмов f: X → Y и g: Y → Z удовлетворяет (g ∘ f)(x) = g(f(x)) для всех x ∈ X.

LaTeX

$$$$ (g \circ f)(x) = g(f(x)) $$$$

Lean4

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

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

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

Разделы

Аффилиация

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