combo_le_max

Mathlib.Analysis.Convex.Segment

URI: https://scilib.ai/kg/mathlib#Convex.combo_le_max

← MathLib Explorer

English

Under a,b ≥ 0 with a+b=1, min x y ≤ a x + b y, viewed in convex context.

Русский

При a,b ≥ 0, a+b=1, min x y ≤ a x + b y в контексте выпуклости.

LaTeX

$$$ a \ge 0, b \ge 0, a+b=1 \Rightarrow \min\{x,y\} \le a x + b y $$$

Lean4

theorem combo_le_max (x y : E) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : a • x + b • y ≤ max x y :=
  (segment_subset_uIcc x y ⟨_, _, ha, hb, hab, rfl⟩).2

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

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

Разделы

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

Аффилиация

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