mul_le_mul_right' — Mathlib

English

Right multiplication is monotone: if b ≤ c, then b·a ≤ c·a for all a, given right-monotone property.

Русский

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

LaTeX

$$$\forall b,c,a \in \alpha,\ b \le c \Rightarrow b\cdot a \le c\cdot a.$$$

Lean4

@[to_additive (attr := gcongr high) add_le_add_right]
theorem mul_le_mul_right' [i : MulRightMono α] {b c : α} (bc : b ≤ c) (a : α) : b * a ≤ c * a :=
  i.elim a bc

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