one_lt_mul' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Assumes right covariance.
The lemma assuming left covariance is `Left.one_lt_mul'`. -/
@[to_additive Right.add_pos' /-- Assumes right covariance.
    The lemma assuming left covariance is `Left.add_pos'`. -/
    ]
theorem one_lt_mul' [MulRightMono α] {a b : α} (ha : 1 < a) (hb : 1 < b) : 1 < a * b :=
  lt_mul_of_one_lt_of_lt' ha hb

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