instTransGt_mathlib

Mathlib.Order.Defs.PartialOrder

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

English

Let α be a preorder. 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

instance : @Trans α α α GT.gt GT.gt GT.gt :=
  ⟨gt_trans⟩

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

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

Разделы

Аффилиация

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