mul_lt_one_of_lt_of_le — Mathlib

English

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

Русский

Если 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.mul_lt_one_of_lt_of_le`. -/
@[to_additive Right.add_neg_of_neg_of_nonpos /-- Assumes right covariance.
          The lemma assuming left covariance is `Left.add_neg_of_neg_of_nonpos`. -/
    ]
theorem mul_lt_one_of_lt_of_le [MulRightStrictMono α] {a b : α} (ha : a < 1) (hb : b ≤ 1) : a * b < 1 :=
  mul_lt_of_lt_one_of_le ha hb

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