min_mul_of_nonneg

Mathlib.Algebra.Order.Ring.Unbundled.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem min_mul_of_nonneg [MulPosMono R] (a b : R) (hc : 0 ≤ c) : min a b * c = min (a * c) (b * c) :=
  (monotone_mul_right_of_nonneg hc).map_min

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

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

Разделы

Аффилиация

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