comm

Mathlib.Order.Defs.Unbundled

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

English

If r is symmetric, then r(a,b) is equivalent to r(b,a).

Русский

Если r симметрично, то r(a,b) эквивално r(b,a).

LaTeX

$$$\\\\forall a,b, \\\\ r(a,b) \\\\Leftrightarrow \\\\ r(b,a).$$$

Lean4

theorem comm [IsSymm α r] {a b : α} : r a b ↔ r b a :=
  ⟨symm, symm⟩

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

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

Разделы

Аффилиация

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