mapₗ_apply_of_measurable — Mathlib

English

For a measurable function f, mapₗ f equals map f as linear maps on measures.

Русский

Для измеримой функции f отображение mapₗ f совпадает с map f как линейные отображения мер.

LaTeX

$$$\\mathrm{map}_{\\ell} f = \\mathrm{map} f$ (as linear maps on measures)$$

Lean4

theorem mapₗ_apply_of_measurable {f : α → β} (hf : Measurable f) (μ : Measure α) : mapₗ f μ = map f μ :=
  by
  simp only [← mapₗ_mk_apply_of_aemeasurable hf.aemeasurable]
  exact mapₗ_congr hf hf.aemeasurable.measurable_mk hf.aemeasurable.ae_eq_mk

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