essSup_apply — Mathlib

English

If g is an order isomorphism, then applying g to the essential supremum equals the essential supremum of the composed function: g(essSup f μ) = essSup (g ∘ f) μ.

Русский

Если g — отображение порядка-изоморфизм, то g(essSup f μ) = essSup (g ∘ f) μ.

LaTeX

$$$$ g(\\operatorname{essSup} f \\mu) = \\operatorname{essSup} (f \\mapsto g(f)) \\mu $$$$

Lean4

theorem essSup_apply {m : MeasurableSpace α} {γ} [CompleteLattice γ] (f : α → β) (μ : Measure α) (g : β ≃o γ) :
    g (essSup f μ) = essSup (fun x => g (f x)) μ :=
  by
  refine OrderIso.limsup_apply g ?_ ?_ ?_ ?_
  all_goals isBoundedDefault

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