instTransAntisymmRelLe

Mathlib.Order.Antisymmetrization

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

English

In the antisymmetrized order, a ≤ b and b < c imply a < c.

Русский

В антисимметризованном порядке a ≤ b и b < c приводят к a < c.

LaTeX

$$$\\forall a,b,c \\in α,\\ AntisymmRel(≤)\\,a\\,b \\to b < c \\to a < c$$$

Lean4

instance : @Trans α α α (AntisymmRel (· ≤ ·)) (· ≤ ·) (· ≤ ·) where trans := le_of_antisymmRel_of_le

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

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

Разделы

Аффилиация

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