add_le_mul' — Mathlib

English

Let R be a semiring with 0 ≤ 1, NeZero 1, MulPosStrictMono, PosMulStrictMono, AddLeftMono. Then a + b ≤ a*b when 2 ≤ a and 2 ≤ b.

Русский

Пусть R — полукольцо с 0 ≤ 1, NeZero 1, MulPosStrictMono, PosMulStrictMono и AddLeftMono. Тогда выполняется a + b ≤ a b при 2 ≤ a и 2 ≤ b.

LaTeX

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

Lean4

theorem add_le_mul' [ZeroLEOneClass R] [NeZero (1 : R)] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R]
    (a2 : 2 ≤ a) (b2 : 2 ≤ b) : a + b ≤ b * a :=
  (le_of_eq (add_comm _ _)).trans (add_le_mul b2 a2)

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