max_mul_mul_left

Mathlib.Algebra.Order.Monoid.Unbundled.MinMax

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

English

Let α be a linearly ordered set with Mul α and MulLeftMono α. Then for all a, b, c ∈ α, max(a·b, a·c) = a · max(b, c).

Русский

Пусть α упорядочено линейно и есть умножение. Тогда max(a·b, a·c) = a · max(b, c).

LaTeX

$$$ \max(a b, a c) = a \cdot \max(b,c) $$$

Lean4

@[to_additive]
theorem max_mul_mul_left (a b c : α) : max (a * b) (a * c) = a * max b c :=
  (monotone_id.const_mul' a).map_max.symm

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

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

Разделы

Аффилиация

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