lt_of_le_of_lt

Mathlib.Order.Basic

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

English

If x1 ≤ y1 and x2 < y2, then x < y in the product order.

Русский

Если x1 ≤ y1 и x2 < y2, то x < y в произведении.

LaTeX

$$$x_1 \le y_1 \land x_2 < y_2 \Rightarrow (x_1,x_2) < (y_1,y_2)$$$

Lean4

protected theorem lt_of_le_of_lt (h₁ : x.1 ≤ y.1) (h₂ : x.2 < y.2) : x < y := by simp [lt_iff, *]

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

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

Разделы

Аффилиация

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