comm

Mathlib.Data.Rel

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

English

Let R be a symmetric relation on α. Then a is related to b by R if and only if b is related to a by R.

Русский

Пусть R — симметричное отношение на α. Тогда a связано с b отношением R тогда и только тогда, когда b связано с a.

LaTeX

$$$a \sim_R b \iff b \sim_R a$$$

Lean4

protected theorem comm [R.IsSymm] : a ~[R] b ↔ b ~[R] a :=
  comm_of (· ~[R] ·)

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

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

Разделы

Аффилиация

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