iSup_mul

Mathlib.Data.NNReal.Basic

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

English

Let a ≥ 0 and f : ι → ℝ≥0. Then (sup_i f(i)) · a = sup_i (f(i) · a).

Русский

Пусть a ≥ 0 и f : ι → ℝ≥0. Тогда (sup_i f(i)) · a = sup_i (f(i) · a).

LaTeX

$$$ \\big(\\sup_{i \\in \\iota} f(i)\\big) \\cdot a = \\sup_{i \\in \\iota} (f(i) \\cdot a) $$$

Lean4

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

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

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

Разделы

Аффилиация

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