min_le_combo

Mathlib.Analysis.Convex.Segment

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

← MathLib Explorer

English

For a,b ≥ 0 with a+b = 1, min{x,y} ≤ a x + b y.

Русский

Для a,b ≥ 0 и a+b = 1 верно: min{x,y} ≤ a x + b y.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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