mul_le_mul_left' — Mathlib

English

If b ≤ c, then a·b ≤ a·c for all a, provided left multiplication is monotone.

Русский

Если b ≤ c, то a·b ≤ a·c для всех a при условии монотонности левого умножения.

LaTeX

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

Lean4

@[to_additive (attr := gcongr high) add_le_add_left]
theorem mul_le_mul_left' [MulLeftMono α] {b c : α} (bc : b ≤ c) (a : α) : a * b ≤ a * c :=
  CovariantClass.elim _ bc

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