inv_eq_self_iff

Mathlib.Data.Rel

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

English

For a relation R on α, R^{-1} = R if and only if R is symmetric.

Русский

Для отношения R на α равно R^{-1} = R тогда и только тогда, когда R симметрично.

LaTeX

$$$R^{-1} = R \iff R \text{ is symmetric}$$$

Lean4

theorem inv_eq_self_iff : R.inv = R ↔ R.IsSymm
    where
  mp hR := ⟨fun a b hab ↦ by rwa [← hR]⟩
  mpr _ := inv_eq_self _

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

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

Разделы

Аффилиация

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