le_iInf_mul

Mathlib.Data.ENNReal.Inv

URI: https://scilib.ai/kg/mathlib#ENNReal.le_iInf_mul

← MathLib Explorer

English

For ENNReal u, v: (⨅ i, u_i) · (⨅ i, v_i) ≤ ⨅ i, u_i · v_i.

Русский

Для функций u, v из индексов выполняется: (⨅ i, u_i) · (⨅ i, v_i) ≤ ⨅ i, (u_i · v_i).

LaTeX

$$$(\\inf_i u_i) \\cdot (\\inf_i v_i) \\leq \\inf_i (u_i \\cdot v_i)$$$

Lean4

theorem le_iInf_mul {ι : Type*} (u v : ι → ℝ≥0∞) : (⨅ i, u i) * ⨅ i, v i ≤ ⨅ i, u i * v i :=
  le_iInf fun i ↦ mul_le_mul' (iInf_le u i) (iInf_le v i)

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

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

Разделы

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

Аффилиация

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