measurable_measure_stieltjesFunction

English

The map a ↦ (hf.stieltjesFunction a).measure is a measurable function of a.

Русский

Замыкаемая функция a ↦ (hf.stieltjesFunction a).measure является измеримой по переменной a.

LaTeX

$$\operatorname{Measurable}\big(\lambda a. (hf.stieltjesFunction a).\mathrm{measure}\big)$$

Lean4

theorem measurable_measure_stieltjesFunction : Measurable fun a ↦ (hf.stieltjesFunction a).measure := by
  apply_rules [StieltjesFunction.measurable_measure, measurable_stieltjesFunction, tendsto_stieltjesFunction_atBot,
    tendsto_stieltjesFunction_atTop]

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