strongLT_of_le_of_strongLT

Mathlib.Order.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem strongLT_of_le_of_strongLT (hab : a ≤ b) (hbc : b ≺ c) : a ≺ c := fun _ ↦ (hab _).trans_lt <| hbc _

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

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

Разделы

Аффилиация

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