iSup_mul_of_nonpos

Mathlib.Data.Real.Pointwise

URI: https://scilib.ai/kg/mathlib#Real.iSup_mul_of_nonpos

English

For r ≤ 0 and f: ι → ℝ, the supremum of iSup equals inf of multiplied: (iSup f(i)) · r = inf_i (f(i) · r).

Русский

Пусть r ≤ 0 и f: ι → ℝ. Тогда (iSup f(i)) · r = inf_i (f(i) · r).

LaTeX

$$$ \Big(\sup_{i} f(i)\Big) \cdot r = \inf_{i} (f(i) \cdot r) $$$

Lean4

theorem iSup_mul_of_nonpos (ha : r ≤ 0) (f : ι → ℝ) : (⨆ i, f i) * r = ⨅ i, f i * r := by
  simp only [Real.mul_iSup_of_nonpos ha, mul_comm]

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

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

Разделы

Аффилиация

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