one_lt_mul_of_lt_of_le — Mathlib

English

If a ≤ 1 and 1 < b, then 1 < a·b.

Русский

Если a ≤ 1 и 1 < b, тогда 1 < a·b.

LaTeX

$$$$\forall a,b \in \alpha:\; a \le 1 \land 1 < b \Rightarrow 1 < a\,b.$$$$

Lean4

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

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