mul_lt_of_mul_lt_right — Mathlib

English

If right multiplication is monotone, then from a·b < c we have a·d < c for any d ≥ b.

Русский

Если правая монотонна, то из a·b < c следует a·d < c при любом d ≥ b.

LaTeX

$$$$ \\forall a,b,c,d \\in \\alpha,\; a \\cdot b < c \\land b \\le d \\Rightarrow a \\cdot d < c $$$$

Lean4

@[to_additive]
theorem mul_lt_of_mul_lt_right [MulRightMono α] {a b c d : α} (h : a * b < c) (hle : d ≤ a) : d * b < c :=
  (mul_le_mul_right' hle b).trans_lt h

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