one_add_le_one_add_mul_one_sub — Mathlib

English

If a + c + b c ≤ b for a, b, c in a ring, then 1 + a ≤ (1 + b)(1 − c).

Русский

Если a + c + bc ≤ b для элементов a, b, c кольца, тогда 1 + a ≤ (1 + b)(1 − c).

LaTeX

$$$a,b,c\\in R,\\ a + c + b c \\le b \\Rightarrow 1 + a \\le (1 + b)(1 - c)$$$

Lean4

theorem one_add_le_one_add_mul_one_sub (h : a + c + b * c ≤ b) : 1 + a ≤ (1 + b) * (1 - c) :=
  by
  rw [mul_one_sub, one_add_mul, le_sub_iff_add_le, add_assoc, ← add_assoc a]
  gcongr

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