min_mul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem min_mul [MulRightMono α] (a b c : α) : min a b * c = min (a * c) (b * c) :=
  mul_left_mono.map_min

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