mul_lt_mul_iff_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem mul_lt_mul_iff_right [MulRightStrictMono α] [MulRightReflectLT α] (a : α) {b c : α} : b * a < c * a ↔ b < c :=
  rel_iff_cov α α (swap (· * ·)) (· < ·) a

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