swap_eq

Mathlib.Logic.Relation

URI: https://scilib.ai/kg/mathlib#Symmetric.swap_eq

English

If a relation r is symmetric, then the swapped relation swap r equals r.

Русский

Если отношение r симметрично, то swap r = r.

LaTeX

$$$\forall r:\alpha\to\alpha\to \mathrm{Prop},\; \mathrm{Symmetric}(r) \Rightarrow \mathrm{swap}(r) = r$$$

Lean4

theorem swap_eq : Symmetric r → swap r = r :=
  Symmetric.flip_eq

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

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

Разделы

Аффилиация

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