mk_le_mk_iff_right

Mathlib.Order.Basic

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

English

On the right coordinate, (a,b1) ≤ (a,b2) iff b1 ≤ b2.

Русский

По правой координате: (a,b1) ≤ (a,b2) эквивалентно b1 ≤ b2.

LaTeX

$$$(a,b_1) \le (a,b_2) \iff b_1 \le b_2$$$

Lean4

theorem mk_le_mk_iff_right : (a, b₁) ≤ (a, b₂) ↔ b₁ ≤ b₂ :=
  and_iff_right le_rfl

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

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

Разделы

Аффилиация

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