mul_lt_one_of_le_of_lt — Mathlib

English

If ha ≤ 1 and hb < 1, then a*b < 1 for left-monotone multiplication.

Русский

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

LaTeX

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

Lean4

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

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