one_add_le_one_sub_mul_one_add — Mathlib

English

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

Русский

Пусть в кольце элементы a, b, c удовлетворяют неравенству a + b + b c ≤ c. Тогда 1 + a ≤ (1 − b)(1 + c).

LaTeX

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

Lean4

theorem one_add_le_one_sub_mul_one_add (h : a + b + b * c ≤ c) : 1 + a ≤ (1 - b) * (1 + c) :=
  by
  rw [one_sub_mul, mul_one_add, le_sub_iff_add_le, add_assoc, ← add_assoc a]
  gcongr

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