instTransGtGe_mathlib

Mathlib.Order.Defs.PartialOrder

URI: https://scilib.ai/kg/mathlib#instTransGtGe_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 \ge c \rightarrow a > c$$$

Lean4

instance : @Trans α α α GT.gt GE.ge GT.gt :=
  ⟨lt_of_lt_of_le'⟩

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

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

Разделы

Аффилиация

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