instTransLeLt_mathlib

Mathlib.Order.Defs.PartialOrder

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

English

Let α be a preorder. For all a, b, c ∈ α, if a ≤ b and b < c, then a < c.

Русский

Пусть α — множество с порядком. Для всех a, b, c ∈ α, если a ≤ b и b < c, тогда a < c.

LaTeX

$$$\forall a,b,c \in \alpha,\ a \le b \land b < c \rightarrow a < c$$$

Lean4

instance : @Trans α α α LE.le LT.lt LT.lt :=
  ⟨lt_of_le_of_lt⟩

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

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

Разделы

Аффилиация

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