le_def

Mathlib.Order.Basic

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

English

The order on the product is defined by the rule (a1,b1) ≤ (a2,b2) ⇔ a1 ≤ a2 ∧ b1 ≤ b2.

Русский

Порядок на произведении задаётся правилом (a1,b1) ≤ (a2,b2) эквивалентно a1 ≤ a2 и b1 ≤ b2.

LaTeX

$$$(a_1,b_1) \le (a_2,b_2) \;\iff\; a_1 \le a_2 \land b_1 \le b_2$$$

Lean4

theorem le_def : x ≤ y ↔ x.1 ≤ y.1 ∧ x.2 ≤ y.2 :=
  .rfl

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

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

Разделы

Аффилиация

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