essSup_add_le — Mathlib

English

For any f, g: α → ℝ≥0∞, the essential supremum of the sum is at most the sum of the essential supremums: essSup (f + g) ≤ essSup f + essSup g.

Русский

Для любых f, g: α → ℝ≥0∞ выполняется essSup (f + g) ≤ essSup f + essSup g.

LaTeX

$$$$ \operatorname{ess\,sup}_{x} (f(x) + g(x)) \le \operatorname{ess\,sup}_{x} f(x) + \operatorname{ess\,sup}_{x} g(x). $$$$

Lean4

theorem essSup_add_le (f g : α → ℝ≥0∞) : essSup (f + g) μ ≤ essSup f μ + essSup g μ :=
  limsup_add_le f g

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