instTransLe_mathlib

Mathlib.Order.Defs.PartialOrder

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

English

The relation ≤ is transitive: if a ≤ b and b ≤ c then a ≤ c.

Русский

Отношение ≤ транзитивно: если a ≤ b и b ≤ c, то a ≤ c.

LaTeX

$$$\\\\forall a,b,c, (a \\le b \\land b \\le c) \\Rightarrow a \\le c$$$

Lean4

instance : @Trans α α α LE.le LE.le LE.le :=
  ⟨le_trans⟩

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

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

Разделы

Аффилиация

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