mul_lt_mul_iff_left — Mathlib

English

Left multiplication by a strictly monotone map preserves strict order: a*b < a*c iff b < c.

Русский

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

LaTeX

$$$[\text{MulLeftStrictMono}(\alpha)]\,[\text{MulLeftReflectLT}(\alpha)]\ (a:\alpha)\;\Rightarrow\; a\cdot b < a\cdot c \iff b < c.$$$

Lean4

@[to_additive (attr := simp)]
theorem mul_lt_mul_iff_left [MulLeftStrictMono α] [MulLeftReflectLT α] (a : α) {b c : α} : a * b < a * c ↔ b < c :=
  rel_iff_cov α α (· * ·) (· < ·) a

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