toRel_symmetric

Mathlib.Data.Sym.Sym2

URI: https://scilib.ai/kg/mathlib#Sym2.toRel_symmetric

English

The ToRel construction yields a symmetric relation.

Русский

Конструкция ToRel задаёт симметричное отношение.

LaTeX

$$$$ \text{The relation } \mathrm{ToRel}(s) \text{ is symmetric.} $$$$

Lean4

theorem toRel_symmetric (s : Set (Sym2 α)) : Symmetric (ToRel s) := fun x y => by simp [eq_swap]

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

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

Разделы

Аффилиация

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