instIsSymmInv

Mathlib.Data.Rel

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

English

If R is symmetric, then its inverse R^{-1} is also symmetric.

Русский

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

LaTeX

$$$R^{-1}$ is symmetric$$

Lean4

instance [R.IsSymm] : R.inv.IsSymm := by simpa

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

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

Разделы

Аффилиация

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