reflTransGen_swap

Mathlib.Logic.Relation

URI: https://scilib.ai/kg/mathlib#Relation.reflTransGen_swap

English

ReflTransGen (swap r) a b is equivalent to ReflTransGen r b a.

Русский

ReflTransGen (swap r) a b эквивалентно ReflTransGen r b a.

LaTeX

$$$$\\operatorname{ReflTransGen} (swap r) a b \\iff \\operatorname{ReflTransGen} r b a$$$$

Lean4

theorem reflTransGen_swap : ReflTransGen (swap r) a b ↔ ReflTransGen r b a :=
  ⟨ReflTransGen.swap, ReflTransGen.swap⟩

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

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

Разделы

Аффилиация

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