isSymm_comp_self

Mathlib.Data.Rel

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

English

If R is symmetric, then R ∘ R is symmetric.

Русский

Если R симметрично, то R ∘ R симметрично.

LaTeX

$$R ∘ R is symmetric$$

Lean4

instance isSymm_comp_self [R.IsSymm] : (R ○ R).IsSymm := by simpa using R.isSymm_comp_inv

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

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

Разделы

Аффилиация

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