mul_le_mul_iff_right — Mathlib

English

Alternative form: left-multiplication by a is order-embedding; 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) \Leftrightarrow (b \le c).$$$

Lean4

@[to_additive (attr := simp)]
theorem mul_le_mul_iff_right [MulRightMono α] [MulRightReflectLE α] (a : α) {b c : α} : b * a ≤ c * a ↔ b ≤ c :=
  rel_iff_cov α α (swap (· * ·)) (· ≤ ·) a

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