max_lt_max_right_iff

Mathlib.Order.MinMax

URI: https://scilib.ai/kg/mathlib#max_lt_max_right_iff

English

max(a,b) < max(a,c) iff b < c and a < c.

Русский

max(a,b) < max(a,c) тогда и только тогда, когда b < c и a < c.

LaTeX

$$$$\max(a,b) < \max(a,c) \iff b < c \land a < c.$$$$

Lean4

theorem max_lt_max_right_iff : max a b < max a c ↔ b < c ∧ a < c :=
  @min_lt_min_right_iff αᵒᵈ _ _ _ _

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

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

Разделы

Аффилиация

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