iSup_div

Mathlib.Data.NNReal.Basic

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

English

For all f : ι → ℝ≥0 and a ∈ ℝ≥0, (sup_i f(i)) / a = sup_i (f(i) / a).

Русский

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

LaTeX

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

Lean4

theorem iSup_div (f : ι → ℝ≥0) (a : ℝ≥0) : (⨆ i, f i) / a = ⨆ i, f i / a := by simp only [div_eq_mul_inv, iSup_mul]

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

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

Разделы

Аффилиация

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