instIsTransGe

Mathlib.Order.RelClasses

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

English

≥ is transitive: if x ≥ y and y ≥ z then x ≥ z.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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