mapₗ_mk_apply_of_aemeasurable — Mathlib

English

If f is almost everywhere measurable with respect to μ, then the linear map mapₗ with f̂ (the aemeasurable.mk) equals the ordinary map f μ.

Русский

Если f измерима почти по μ, то линейное отображение mapₗ с f̂ совпадает с обычным отображением map f μ.

LaTeX

$$$\\mathrm{map}_{\\ell} f \\; \\mu = \\mathrm{map} f \\; \\mu$$$

Lean4

theorem mapₗ_mk_apply_of_aemeasurable {f : α → β} (hf : AEMeasurable f μ) : mapₗ (hf.mk f) μ = map f μ := by
  simp [map, hf]

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