comp_id

Mathlib.Data.Rel

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

English

Composition with the identity leaves the relation unchanged: R ○ id = R.

Русский

Композиция с единичным отношением не изменяет отношение: R ○ id = R.

LaTeX

$$R \circ \mathrm{SetRel.id} = R$$

Lean4

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

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

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

Разделы

Аффилиация

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