isSymm_inv_comp

Mathlib.Data.Rel

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

English

The composition R^{-1} ∘ R is symmetric.

Русский

Обратная композиция R^{-1} ∘ R симметрична.

LaTeX

$$(R^{-1} ∘ R) is symmetric$$

Lean4

instance isSymm_inv_comp : (R.inv ○ R).IsSymm :=
  isSymm_comp_inv

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

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

Разделы

Аффилиация

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