transitive_gt

Mathlib.Order.RelClasses

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

English

The relation > is transitive: if a > b and b > c, then a > c.

Русский

Отношение > транзитивно: если a > b и b > c, то a > c.

LaTeX

$$$\forall a,b,c \in \alpha,\ a > b \land b > c \rightarrow a > c$$$

Lean4

theorem transitive_gt [Preorder α] : Transitive (@GT.gt α _) :=
  transitive_of_trans _

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

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

Разделы

Аффилиация

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