mk_le_mk

Mathlib.Order.Basic

URI: https://scilib.ai/kg/mathlib#Prod.GCongr.mk_le_mk

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) \le (a_2,b_2) \;\Leftarrow\; a_1 \le a_2 \land b_1 \le b_2$$$

Lean4

@[gcongr]
theorem mk_le_mk (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : (a₁, b₁) ≤ (a₂, b₂) :=
  ⟨ha, hb⟩

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

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

Разделы

Аффилиация

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