max_mul_of_nonneg

Mathlib.Algebra.Order.Ring.Unbundled.Basic

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

English

Let R be a semiring with MulPosMono. If 0 ≤ c, then max(a,b) * c = max(a*c, b*c).

Русский

Пусть R — полукольцо с MulPosMono. Если 0 ≤ c, то max(a,b)·c = max(a·c, b·c).

LaTeX

$$$0 \le c \Rightarrow \max(a,b) \cdot c = \max(a c, b c)$$$

Lean4

theorem max_mul_of_nonneg [MulPosMono R] (a b : R) (hc : 0 ≤ c) : max a b * c = max (a * c) (b * c) :=
  (monotone_mul_right_of_nonneg hc).map_max

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

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

Разделы

Аффилиация

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