stronglyMeasurable_stieltjesFunction

English

For any real x, the map a ↦ hf.stieltjesFunction a x is strongly measurable.

Русский

Для любого реального x отображение a ↦ hf.stieltjesFunction a x является сильно измеримой.

LaTeX

$$$$ \\text{StronglyMeasurable}(a \\mapsto hf.stieltjesFunction a x). $$$$

Lean4

theorem stronglyMeasurable_stieltjesFunction (x : ℝ) : StronglyMeasurable fun a ↦ hf.stieltjesFunction a x :=
  (measurable_stieltjesFunction hf x).stronglyMeasurable

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