max_mul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem max_mul [MulRightMono α] (a b c : α) : max a b * c = max (a * c) (b * c) :=
  mul_left_mono.map_max

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