trans

Mathlib.Order.Antisymmetrization

URI: https://scilib.ai/kg/mathlib#AntisymmRel.trans

← MathLib Explorer

English

If AntisymmRel r a b and AntisymmRel r b c, then AntisymmRel r a c.

Русский

Если AntisymmRel r a b и AntisymmRel r b c, то AntisymmRel r a c.

LaTeX

$$$\mathrm{AntisymmRel}(r)\,a\,b \land \mathrm{AntisymmRel}(r)\,b\,c \Rightarrow \mathrm{AntisymmRel}(r)\,a\,c$$$

Lean4

@[trans]
theorem trans [IsTrans α r] (hab : AntisymmRel r a b) (hbc : AntisymmRel r b c) : AntisymmRel r a c :=
  ⟨_root_.trans hab.1 hbc.1, _root_.trans hbc.2 hab.2⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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