mk_lt_mk_iff_left

Mathlib.Order.Basic

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

English

(a1,b) < (a2,b) iff a1 < a2.

Русский

(a1,b) < (a2,b) эквивалентно a1 < a2.

LaTeX

$$$(a_1,b) < (a_2,b) \iff a_1 < a_2$$

Lean4

theorem mk_lt_mk_iff_left : (a₁, b) < (a₂, b) ↔ a₁ < a₂ :=
  lt_iff_lt_of_le_iff_le' mk_le_mk_iff_left mk_le_mk_iff_left

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

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

Разделы

Аффилиация

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