le_trans

Mathlib.Order.Defs.PartialOrder

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

English

If a ≤ b and b ≤ c, then a ≤ c.

Русский

Если a ≤ b и b ≤ c, то a ≤ c.

LaTeX

$$$a \\le b \\\\land b \\le c \\\\Rightarrow a \\le c$$$

Lean4

/-- The relation `≤` on a preorder is transitive. -/
theorem le_trans : a ≤ b → b ≤ c → a ≤ c :=
  Preorder.le_trans _ _ _

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

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

Разделы

Аффилиация

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