sSup_div

Mathlib.Data.ENNReal.Inv

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

English

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

Русский

Для s ⊆ ENNReal и a ∈ ENNReal: sSup s / a = ⨆_{b ∈ s} (b / a).

LaTeX

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

Lean4

theorem sSup_div (s : Set ℝ≥0∞) (a : ℝ≥0∞) : sSup s / a = ⨆ b ∈ s, b / a :=
  sSup_mul ..

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

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

Разделы

Аффилиация

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