symm

Mathlib.Data.Sym.Sym2

URI: https://scilib.ai/kg/mathlib#Sym2.Rel.symm

English

Sym2.Rel is symmetric: if x relates to y, then y relates to x.

Русский

Sym2.Rel симметрично: если x связано с y, то и y связано с x.

LaTeX

$$$\mathrm{Rel}\,\alpha\; x\, y \rightarrow \mathrm{Rel}\,\alpha\; y\, x$$$

Lean4

@[symm]
theorem symm {x y : α × α} : Rel α x y → Rel α y x := by aesop (rule_sets := [Sym2])

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

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

Разделы

Аффилиация

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