mul_lt_mul_iff_right₀ — Mathlib

English

If a > 0 and a is strictly positive on the left, then a·b < a·c iff b < c.

Русский

Если a > 0 и левая часть положительна, то a·b < a·c эквивалентно b < c.

LaTeX

$$[PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) : a * b < a * c \iff b < c$$

Lean4

@[simp]
theorem mul_lt_mul_iff_right₀ [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) : a * b < a * c ↔ b < c :=
  @rel_iff_cov α>0 α (fun x y => x * y) (· < ·) _ _ ⟨a, a0⟩ _ _

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