comp_assoc

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.comp_assoc

English

Composition of relations is associative: (R ○ S) ○ t = R ○ (S ○ t).

Русский

Операция композиции отношений ассоциативна: (R ○ S) ○ t = R ○ (S ○ t).

LaTeX

$$(R \circ S) \circ t = R \circ (S \circ t)$$

Lean4

theorem comp_assoc (R : SetRel α β) (S : SetRel β γ) (t : SetRel γ δ) : (R ○ S) ○ t = R ○ (S ○ t) := by aesop

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

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

Разделы

Аффилиация

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