sSup_mul

Mathlib.Data.ENNReal.Inv

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

English

For a ∈ ENNReal and s ⊆ ENNReal, sSup s · a = ⨆ b ∈ s, b · a.

Русский

Пусть a ∈ ENNReal и s ⊆ ENNReal. Тогда sSup s · a = ⨆_{b ∈ s} (b · a).

LaTeX

$$$\\operatorname{sSup} s \\cdot a = \\displaystyle \\sup_{b \\in s} b \\cdot a$$$

Lean4

theorem sSup_mul {a : ℝ≥0∞} : sSup s * a = ⨆ b ∈ s, b * a := by simp only [sSup_eq_iSup, iSup_mul]

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

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

Разделы

Аффилиация

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