one_le_mul — Mathlib

English

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 \land b \le 1 \Rightarrow a\,b \le 1.$$$$

Lean4

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

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