add_le_mul_of_left_le_right — Mathlib

English

Let R be a semiring with 0 ≤ 1, NeZero 1, MulPosStrictMono, AddLeftMono. If 2 ≤ a and a ≤ b, then a + b ≤ a b.

Русский

Пусть R — полукольцо с 0 ≤ 1, не-ноль 1, монотонностью умножения слева и монотонностью сложения слева. Если 2 ≤ a и a ≤ b, то a + b ≤ a b.

LaTeX

$$$(2 \le a) \land (a \le b) \Rightarrow a + b \le a b$$$

Lean4

theorem add_le_mul_of_left_le_right [ZeroLEOneClass R] [NeZero (1 : R)] [MulPosStrictMono R] [AddLeftMono R]
    (a2 : 2 ≤ a) (ab : a ≤ b) : a + b ≤ a * b :=
  have : 0 < b :=
    calc
      0 < 2 := zero_lt_two
      _ ≤ a := a2
      _ ≤ b := ab
  calc
    a + b ≤ b + b := add_le_add_right ab b
    _ = 2 * b := (two_mul b).symm
    _ ≤ a * b := (mul_le_mul_iff_left₀ this).mpr a2

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