compRel_assoc

Mathlib.Topology.UniformSpace.Defs

URI: https://scilib.ai/kg/mathlib#compRel_assoc

English

Relation composition 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 compRel_assoc {r s t : Set (α × α)} : r ○ s ○ t = r ○ (s ○ t) := by ext ⟨a, b⟩; simp only [mem_compRel]; tauto

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

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

Разделы

Аффилиация

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