le_of_le_of_antisymmRel

Mathlib.Order.Antisymmetrization

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

English

If a ≤ b and AntisymmRel (≤) b c, then a ≤ c.

Русский

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

LaTeX

$$$a \le b \land \mathrm{AntisymmRel}(\le)\,b\,c \Rightarrow a \le c$$$

Lean4

theorem le_of_le_of_antisymmRel (h₁ : a ≤ b) (h₂ : AntisymmRel (· ≤ ·) b c) : a ≤ c :=
  h₁.trans h₂.le

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

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

Разделы

Аффилиация

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