right

Mathlib.Order.Antisymmetrization

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.GCongr.AntisymmRel.right

English

From AntisymmRel r a b one can read off the right component, namely r b a.

Русский

Из AntisymmRel r a b следует правая компонента: r b a.

LaTeX

$$$\text{AntisymmRel}(r)\,a\,b \to r\,b\,a$$$

Lean4

theorem right (h : AntisymmRel r a b) : r b a :=
  h.2

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

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

Разделы

Аффилиация

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