add_sub_div_two_lt

Mathlib.Algebra.Order.Field.Basic

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

← MathLib Explorer

English

If a < b, then a + (b - a)/2 < b.

Русский

Если a < b, то a + (b - a)/2 < b.

LaTeX

$$$a < b \Rightarrow a + \frac{b - a}{2} < b$$$

Lean4

theorem add_sub_div_two_lt (h : a < b) : a + (b - a) / 2 < b := by
  rwa [← div_sub_div_same, sub_eq_add_neg, add_comm (b / 2), ← add_assoc, ← sub_eq_add_neg, ← lt_sub_iff_add_lt,
    sub_self_div_two, sub_self_div_two, div_lt_div_iff_of_pos_right (zero_lt_two' α)]

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

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

Разделы

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

Аффилиация

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