mul_le_of_le_of_le_one — Mathlib

English

If b ≤ c and a ≤ 1, then b·a ≤ c for any a,b,c ∈ α with left-monotone multiplication.

Русский

Если b ≤ c и a ≤ 1, то b·a ≤ c при левом монотонном умножении.

LaTeX

$$$$\forall a,b,c \in \alpha:\; b \le c \land a \le 1 \Rightarrow b\,a \le c.$$$$

Lean4

@[to_additive]
theorem mul_le_of_le_of_le_one [MulLeftMono α] {a b c : α} (hbc : b ≤ c) (ha : a ≤ 1) : b * a ≤ c :=
  calc
    b * a ≤ b * 1 := mul_le_mul_left' ha b
    _ = b := (mul_one b)
    _ ≤ c := hbc

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