id_comp

Mathlib.Data.Rel

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

English

Let R be a relation between α and β. The identity relation on α acts as a left identity for composition, so id_α ○ R = R.

Русский

Пусть R — отношение между α и β. Идентичное отношение на α слева по композиции даёт то же отношение: id_α ○ R = R.

LaTeX

$$$id_\alpha \circ R = R$$$

Lean4

@[simp]
theorem id_comp (R : SetRel α β) : .id ○ R = R := by aesop

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

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

Разделы

Аффилиация

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