one_sub_le_one_add_mul_one_sub

Mathlib.Algebra.Order.Ring.Defs

URI: https://scilib.ai/kg/mathlib#one_sub_le_one_add_mul_one_sub

← MathLib Explorer

English

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

Русский

Если c + bc ≤ a + b, тогда 1 − a ≤ (1 + b)(1 − c).

LaTeX

$$$c + bc \\le a + b \\Rightarrow 1 - a \\le (1 + b)(1 - c)$$$

Lean4

theorem one_sub_le_one_add_mul_one_sub (h : c + b * c ≤ a + b) : 1 - a ≤ (1 + b) * (1 - c) :=
  by
  rw [mul_one_sub, one_add_mul, sub_le_sub_iff, add_assoc, add_comm b]
  gcongr

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru