mul_max_of_nonneg

Mathlib.Algebra.Order.Ring.Unbundled.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_max_of_nonneg [PosMulMono R] (b c : R) (ha : 0 ≤ a) : a * max b c = max (a * b) (a * c) :=
  (monotone_mul_left_of_nonneg ha).map_max

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

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

Разделы

Аффилиация

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