measurable_map — Mathlib

English

If f: α → β is measurable, then the map sending a measure μ on α to its pushforward measure map f μ on β is measurable.

Русский

Пусть f: α → β измеримо. Тогда отображение μ ↦ map f μ из мер на α в меры на β является измеримым.

LaTeX

$$$\\text{Measurable } f \\rightarrow \\text{Measurable }(\\mu \\mapsto \\text{map }f\\,\\mu).$$$

Lean4

@[fun_prop]
theorem measurable_map (f : α → β) (hf : Measurable f) : Measurable fun μ : Measure α => map f μ :=
  by
  refine measurable_of_measurable_coe _ fun s hs => ?_
  simp_rw [map_apply hf hs]
  exact measurable_coe (hf hs)

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