mul_le_mul_iff_left — Mathlib

English

For any a with left multiplication preserving order, a·b ≤ a·c iff b ≤ c.

Русский

Для любого a, при условии сохранения порядка левой операцией умножения, a·b ≤ a·c эквивалентно b ≤ c.

LaTeX

$$$[\text{MulLeftMono}(\alpha)]\,[\text{MulLeftReflectLE}(\alpha)]\ (a:\alpha)\;\Rightarrow\; a\cdot b \le a\cdot c \iff b \le c.$$$

Lean4

@[to_additive (attr := simp)]
theorem mul_le_mul_iff_left [MulLeftMono α] [MulLeftReflectLE α] (a : α) {b c : α} : a * b ≤ a * c ↔ b ≤ c :=
  rel_iff_cov α α (· * ·) (· ≤ ·) a

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