swap_eq_iff

Mathlib.Logic.Relation

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

English

Equality of swap r and r is equivalent to r being symmetric.

Русский

Равенство swap r и r эквивалентно тому, что r симметрично.

LaTeX

$$$\mathrm{swap}(r) = r \iff \mathrm{Symmetric}(r)$$$

Lean4

theorem swap_eq_iff : swap r = r ↔ Symmetric r :=
  flip_eq_iff

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

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

Разделы

Аффилиация

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