instTransAntisymmRelLeLt

Mathlib.Order.Antisymmetrization

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

English

If a ≤ b in the antisymmetric sense and b < c, then 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 := lt_of_antisymmRel_of_lt

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

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

Разделы

Аффилиация

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