le_of_antisymmRel_of_le

Mathlib.Order.Antisymmetrization

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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