inv_eq_self

Mathlib.Data.Rel

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

English

If R is symmetric, then its inverse equals itself: R^{-1} = R.

Русский

Если R симметрично, то обратное отношение R^{-1} равно самому R.

LaTeX

$$$R^{-1} = R$$$

Lean4

@[simp]
theorem inv_eq_self [R.IsSymm] : R.inv = R := by ext; exact R.comm

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

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

Разделы

Аффилиация

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