essSup_const_mul — Mathlib

English

Let a be a nonnegative extended real number and f a function to ℝ≥0∞. Then the essential supremum commutes with multiplication by a: essSup_x (a · f(x)) = a · essSup_x f(x).

Русский

Пусть a ∈ ℝ≥0∞ и f: α → ℝ≥0∞. Тогда essSup_x (a · f(x)) = a · essSup_x f(x).

LaTeX

$$$$ \operatorname{ess\,sup}_{x} (a \cdot f(x)) = a \cdot \operatorname{ess\,sup}_{x} f(x) $$$$

Lean4

theorem essSup_const_mul {a : ℝ≥0∞} : essSup (fun x : α => a * f x) μ = a * essSup f μ :=
  limsup_const_mul

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