max_le_max_left

Mathlib.Order.MinMax

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

English

If a ≤ b, then max c a ≤ max c b.

Русский

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

LaTeX

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

Lean4

theorem max_le_max_left (c) (h : a ≤ b) : max c a ≤ max c b :=
  sup_le_sup_left h c

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

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

Разделы

Аффилиация

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