mul_lt_one' — Mathlib

English

If a ≤ 1 and b ≤ 1, then a*b ≤ 1 (left-covariant form).

Русский

Если 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.mul_lt_one'`. -/
@[to_additive /-- Assumes left covariance.
    The lemma assuming right covariance is `Right.add_neg'`. -/
    ]
theorem mul_lt_one' [MulLeftMono α] {a b : α} (ha : a < 1) (hb : b < 1) : a * b < 1 :=
  mul_lt_of_lt_of_lt_one' ha hb

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