mul_lt_of_le_one_of_lt — Mathlib

English

In a preorder monoid with right monotone multiplication, if a ≤ 1 and b < c, then a·b < c.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mul_lt_of_le_one_of_lt [MulRightMono α] {a b c : α} (ha : a ≤ 1) (hb : b < c) : a * b < c :=
  calc
    a * b ≤ 1 * b := mul_le_mul_right' ha b
    _ = b := (one_mul b)
    _ < c := hb

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