lt_max_of_lt_left

Mathlib.Order.MinMax

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

English

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

Русский

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

LaTeX

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

Lean4

theorem lt_max_of_lt_left (h : a < b) : a < max b c :=
  h.trans_le (le_max_left b c)

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

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

Разделы

Аффилиация

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