one_le_mul — Mathlib

English

In a preorder monoid with right monotone multiplication, if a ≤ 1 and b ≤ 1, then a·b ≤ 1.

Русский

В предельном моноиде с правой монотонностью умножения, если a ≤ 1 и b ≤ 1, то a·b ≤ 1.

LaTeX

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

Lean4

/-- Assumes right covariance.
The lemma assuming left covariance is `Left.one_le_mul`. -/
@[to_additive Right.add_nonneg /-- Assumes right covariance.
    The lemma assuming left covariance is `Left.add_nonneg`. -/
    ]
theorem one_le_mul [MulRightMono α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b :=
  le_mul_of_one_le_of_le ha hb

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