symm

Mathlib.Data.Rel

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

English

Let R be a symmetric relation on a set α. If a is related to b by R, then b is related to a by R.

Русский

Пусть R — симметричное отношение на множестве α. Если a связано с b отношением R, то и наоборот: b связано с a.

LaTeX

$$$a \sim_R b \Rightarrow b \sim_R a$$$

Lean4

protected theorem symm [R.IsSymm] (hab : a ~[R] b) : b ~[R] a :=
  symm_of (· ~[R] ·) hab

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

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

Разделы

Аффилиация

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