mul_max — Mathlib

English

Let α be a type with LinearOrder and left-monotone multiplication. Then a · max(b,c) = max(a·b, a·c).

Русский

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

LaTeX

$$$$ \\forall a,b,c \\in \\alpha,\; a \\cdot \\max(b,c) = \\max(a\\cdot b, a\\cdot c) $$$$

Lean4

@[to_additive]
theorem mul_max [MulLeftMono α] (a b c : α) : a * max b c = max (a * b) (a * c) :=
  mul_right_mono.map_max

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