smul_measure — Mathlib

English

If f is a measurable function from α to ℝ≥0∞, then the map μ ↦ f x • μ defines a measurable map from measures to measures.

Русский

Если f измерима, то отображение μ ↦ f x · μ задаёт измеримое отображение от мер к мерам.

LaTeX

$$$\text{Measurable.smul_measure}$: Measurable f → ∀ μ, Measurable (x \mapsto f(x) \cdot μ)$$$

Lean4

@[fun_prop]
theorem _root_.Measurable.smul_measure {f : α → ℝ≥0∞} (hf : Measurable f) (μ : Measure β) :
    Measurable (fun x ↦ f x • μ) :=
  by
  refine Measure.measurable_of_measurable_coe _ fun s hs ↦ ?_
  simp only [Measure.smul_apply, smul_eq_mul]
  fun_prop

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