instIsTransGt

Mathlib.Order.RelClasses

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

English

Gt is transitive: if x > y and y > z then x > z.

Русский

Gt транзитивно: если x > y и y > z, то x > z.

LaTeX

$$$ \\forall x,y,z : α,\ x > y \\land y > z \\Rightarrow x > z $$$

Lean4

instance [Preorder α] : IsTrans α (· > ·) :=
  IsTrans.swap _

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

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

Разделы

Аффилиация

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