iSup_div

Mathlib.Data.ENNReal.Inv

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

English

For f : I → ENNReal and a ∈ ENNReal, iSup f / a = ⨆ i, f(i) / a.

Русский

Для f : I → ENNReal и a ∈ ENNReal верно: \$ \\big(\\sup_i f_i\\big)/a = \\sup_i (f_i / a) \$.

LaTeX

$$$\\displaystyle i\\!\\!\\!\\! \\left(\\sup_i f_i\\right) / a = \\displaystyle \\sup_i \\left( f_i / a \\right)$$$

Lean4

theorem iSup_div (f : ι → ℝ≥0∞) (a : ℝ≥0∞) : iSup f / a = ⨆ i, f i / a :=
  iSup_mul ..

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

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

Разделы

Аффилиация

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