iSup_mul

Mathlib.Data.ENNReal.Inv

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

English

Let f : I → ENNReal and a ∈ ENNReal. Then (sup_i f(i)) · a = sup_i (f(i) · a).

Русский

Пусть f : I → ENNReal и a ∈ ENNReal. Тогда (sup_i f(i)) · a = sup_i (f(i) · a).

LaTeX

$$$\\left(\\sup_i f_i\\right) \\cdot a = \\sup_i (f_i \\cdot a)$$$

Lean4

theorem iSup_mul (f : ι → ℝ≥0∞) (a : ℝ≥0∞) : (⨆ i, f i) * a = ⨆ i, f i * a := by simp [mul_comm, mul_iSup]

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

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

Разделы

Аффилиация

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