essSup_trim — Mathlib

English

Under trimming, the essential supremum of f remains the same: essSup f (μ.trim hm) = essSup f μ for measurable f.

Русский

При обрезке essSup f не изменяется: essSup f (μ.trim hm) = essSup f μ для измеримой f.

LaTeX

$$essSup f (μ.trim hm) = essSup f μ$$

Lean4

theorem essSup_trim (hm : m ≤ m0) {f : α → ℝ≥0∞} (hf : Measurable[m] f) : essSup f (μ.trim hm) = essSup f μ :=
  by
  simp_rw [essSup]
  exact limsup_trim hm hf

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