lt_mul_of_one_lt_of_lt — Mathlib

English

If a·b < c and 1 ≤ b, then a < c, in a left-monotone setting.

Русский

Если a·b < c и 1 ≤ b, то a < c, в условиях левой монотонности.

LaTeX

$$$\forall a,b,c\in \alpha\; (a b < c) \land (1 \le b) \Rightarrow a < c$$$

Lean4

@[to_additive]
theorem lt_mul_of_one_lt_of_lt [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

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