min_mul_mul_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem min_mul_mul_left (a b c : α) : min (a * b) (a * c) = a * min b c :=
  (monotone_id.const_mul' a).map_min.symm

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