lt_max_of_lt_right

Mathlib.Order.MinMax

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

English

If a < c, then a < max(b, c).

Русский

Если a < c, то a < max(b,c).

LaTeX

$$$a < c \Rightarrow a < \max(b,c)$$$

Lean4

theorem lt_max_of_lt_right (h : a < c) : a < max b c :=
  h.trans_le (le_max_right b c)

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

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

Разделы

Аффилиация

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