mul_lt_of_lt_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 < 1) \to (b < c) \Rightarrow a b < c$$$

Lean4

@[to_additive]
theorem mul_lt_of_lt_one_of_lt' [MulRightMono α] {a b c : α} (ha : a < 1) (hbc : b < c) : a * b < c :=
  mul_lt_of_le_one_of_lt ha.le hbc

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