instTransGeGt_mathlib

Mathlib.Order.Defs.PartialOrder

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

Lean4

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

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

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

Разделы

Аффилиация

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