instIsStrictOrderGt

Mathlib.Order.RelClasses

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

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