one_lt_mul' — Mathlib

English

Let α be a multiplicative monoid with unit and a preorder, and assume left covariance of multiplication. If a and b are strictly greater than 1, then their product a·b is strictly greater than 1.

Русский

Пусть α — умножаемый моноид с единицей и отношением порядка, и предположим левую ковариантность умножения. Если элементы a и b строго больше 1, то их произведение a·b строго больше 1.

LaTeX

$$$\forall a,b\in \alpha\; (1

Lean4

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

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