mk_lt_mk_of_lt_of_le

Mathlib.Order.Basic

URI: https://scilib.ai/kg/mathlib#Prod.mk_lt_mk_of_lt_of_le

English

If a1 < a2 and b1 ≤ b2 then (a1,b1) < (a2,b2).

Русский

Если a1 < a2 и b1 ≤ b2, то (a1,b1) < (a2,b2).

LaTeX

$$$(a_1,b_1) < (a_2,b_2) \Leftarrow a_1 < a_2 \land b_1 \le b_2$$$

Lean4

theorem mk_lt_mk_of_lt_of_le (h₁ : a₁ < a₂) (h₂ : b₁ ≤ b₂) : (a₁, b₁) < (a₂, b₂) := by simp [lt_iff, *]

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

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

Разделы

Аффилиация

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