transitive_ge

Mathlib.Order.RelClasses

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

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 \ge b \land b \ge c \rightarrow a \ge c$$$

Lean4

theorem transitive_ge [Preorder α] : Transitive (@GE.ge α _) :=
  transitive_of_trans _

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

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

Разделы

Аффилиация

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