lt_mul_of_one_lt_of_le — Mathlib

English

If a > 1 and b ≤ c in a preorder monoid with right monotone multiplication, then b ≤ a·c.

Русский

Если a > 1 и b ≤ c в пределовом моноиде с правой монотонностью умножения, то b ≤ a·c.

LaTeX

$$$\forall a,b,c\in \alpha\; (a > 1) \to (b \le c) \Rightarrow b \le a c$$$

Lean4

@[to_additive]
theorem lt_mul_of_one_lt_of_le [MulRightStrictMono α] {a b c : α} (ha : 1 < a) (hbc : b ≤ c) : b < a * c :=
  calc
    b ≤ c := hbc
    _ = 1 * c := (one_mul c).symm
    _ < a * c := mul_lt_mul_right' ha c

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