mul_lt_mul_right' — Mathlib

English

Right multiplication by a strictly monotone map is strictly monotone: if b < c then b*a < c*a.

Русский

Правое умножение на строго монотонную карту сохраняет строгость: если b < c, тогда b·a < c·a.

LaTeX

$$$[\text{MulRightStrictMono}(\alpha)]\,{b,c,a} \; (b < c) \Rightarrow b\cdot a < c\cdot a.$$$

Lean4

@[to_additive (attr := gcongr high) add_lt_add_right]
theorem mul_lt_mul_right' [i : MulRightStrictMono α] {b c : α} (bc : b < c) (a : α) : b * a < c * a :=
  i.elim a bc

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