mul_le_of_le_one_of_le — Mathlib

English

Let α be a monoid with unit and preorder, and assume right monotonicity of multiplication. If a ≤ 1 and b ≤ c, then a·b ≤ c.

Русский

Пусть α — моноид с единицей и порядком, и умножение монотонно по правой части. Если a ≤ 1 и b ≤ c, то a·b ≤ c.

LaTeX

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

Lean4

@[to_additive]
theorem mul_le_of_le_one_of_le [MulRightMono α] {a b c : α} (ha : a ≤ 1) (hbc : b ≤ c) : a * b ≤ c :=
  calc
    a * b ≤ 1 * b := mul_le_mul_right' ha b
    _ = b := (one_mul b)
    _ ≤ c := hbc

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