instTransLtAntisymmRelLe

Mathlib.Order.Antisymmetrization

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

English

If a < b and b ≤ c in antisymmetric sense, then a < c.

Русский

Если a < b и b ≤ c в антисимметрическом отношении, то a < c.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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