instTransGe_mathlib

Mathlib.Order.Defs.PartialOrder

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

Lean4

instance : @Trans α α α GE.ge GE.ge GE.ge :=
  ⟨ge_trans⟩

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

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

Разделы

Аффилиация

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