instIsTransLe

Mathlib.Order.RelClasses

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

English

≤ is transitive: if x ≤ y and y ≤ z then x ≤ z.

Русский

≤ транзитивно: если x ≤ y и y ≤ z, то x ≤ z.

LaTeX

$$$ \\forall x,y,z : α,\ x \\le y \\land y \\le z \\Rightarrow x \\le z $$$

Lean4

instance [Preorder α] : IsTrans α (· ≤ ·) :=
  ⟨@le_trans _ _⟩

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

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

Разделы

Аффилиация

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