mul_lt_mul_iff_left — Mathlib

English

For a > 0, a · b ≤ a · c implies b ≤ c (left cancellation for ≤).

Русский

Для a > 0, если a · b ≤ a · c, то b ≤ c (левое затухание неравенств ≤).

LaTeX

$$$\forall a,b,c \in \mathrm{Ordinal},\ a > 0 \rightarrow (a \cdot b \le a \cdot c \Rightarrow b \le c)$$$

Lean4

@[deprecated mul_lt_mul_iff_right₀ (since := "2025-08-26")]
theorem mul_lt_mul_iff_left {a b c : Ordinal} (a0 : 0 < a) : a * b < a * c ↔ b < c :=
  mul_lt_mul_iff_right₀ a0

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