transitive_le

Mathlib.Order.RelClasses

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

English

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

Русский

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

LaTeX

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

Lean4

theorem transitive_le [Preorder α] : Transitive (@LE.le α _) :=
  transitive_of_trans _

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

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

Разделы

Аффилиация

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