graph_comp

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#Function.graph_comp

English

The graph of the composition f ∘ g equals the composition of the graphs, graph g composed with graph f.

Русский

Граф композиции f ∘ g равен композиции графов: граф g затем граф f.

LaTeX

$$$\text{graph}(f \circ g) = \text{graph}(g) \circ \text{graph}(f)$$$

Lean4

theorem graph_comp (f : β → γ) (g : α → β) : graph (f ∘ g) = graph g ○ graph f := by aesop

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

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

Разделы

Аффилиация

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