instIsTransAntisymmRel

Mathlib.Order.Antisymmetrization

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

English

If r is transitive, then AntisymmRel r is transitive.

Русский

Если r транзитивен, то AntisymmRel r транзитивен.

LaTeX

$$$\mathrm{IsTrans}(\alpha, r) \Rightarrow \mathrm{IsTrans}(\alpha, \operatorname{AntisymmRel}(r))$$$

Lean4

instance [IsTrans α r] : IsTrans α (AntisymmRel r) where trans _ _ _ := .trans

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

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

Разделы

Аффилиация

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