one_lt_mul_of_lt_of_le — Mathlib

English

If a < 1 and b ≤ 1, then a·b < 1 in a right-strict-monotone setting.

Русский

Если a < 1 и b ≤ 1, то a·b < 1 в условиях правого строгого монотонного умножения.

LaTeX

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

Lean4

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

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