stronglyMeasurable_stieltjesOfMeasurableRat

English

For each x ∈ ℝ, the function a ↦ (stieltjesOfMeasurableRat f hf a).toFun x is strongly measurable in a.

Русский

Для каждого фиксированного x ∈ ℝ функция a ↦ (stieltjesOfMeasurableRat f hf a).toFun x является сильно измеримой по a.

LaTeX

$$\operatorname{StronglyMeasurable}\big( a \mapsto (stieltjesOfMeasurableRat\ f\ hf\ a).toFun\, x \big)$$

Lean4

theorem stronglyMeasurable_stieltjesOfMeasurableRat (hf : Measurable f) (x : ℝ) :
    StronglyMeasurable fun a ↦ stieltjesOfMeasurableRat f hf a x :=
  IsMeasurableRatCDF.stronglyMeasurable_stieltjesFunction _ x

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