inv_id

Mathlib.Data.Rel

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

English

The inverse of the identity relation on α is the identity relation itself: (id)^{-1} = id.

Русский

Обратное тождественного отношения на α равно самому тождественному отношению: id^{-1} = id.

LaTeX

$$ (\mathrm{id})^{-1} = \mathrm{id}$$

Lean4

theorem inv_id : (.id : SetRel α α).inv = .id := by aesop

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

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

Разделы

Аффилиация

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