instIsStrictOrderLt

Mathlib.Order.RelClasses

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

English

Let α be a preorder. Then < is a strict order: it is irreflexive and transitive.

Русский

Пусть α — предпорядок. Тогда < является строгим порядком: иррефлексивен и транзитивен.

LaTeX

$$$\forall a \in \alpha\, \neg (a < a) \land \forall a,b,c \in \alpha\ (a < b \land b < c \rightarrow a < c)$$$

Lean4

instance [Preorder α] : IsStrictOrder α (· < ·) where

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

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

Разделы

Аффилиация

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