left_lt_add_div_two

Mathlib.Algebra.Order.Field.Basic

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

English

For any a,b, a < (a+b)/2 iff a < b.

Русский

Для любых a,b, выполняется a < (a+b)/2 тогда и только тогда, когда a < b.

LaTeX

$$$a < \\dfrac{a+b}{2} \\iff a < b$$$

Lean4

theorem left_lt_add_div_two : a < (a + b) / 2 ↔ a < b := by simp [lt_div_iff₀, mul_two]

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

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

Разделы

Аффилиация

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