measure_stieltjesOfMeasurableRat_Iic

English

For any a, x ∈ ℝ, the measure of (−∞, x] under (stieltjesOfMeasurableRat f hf a).measure equals the real value of stieltjesOfMeasurableRat at x, i.e., ENNReal.ofReal (stieltjesOfMeasurableRat f hf a x).

Русский

Для любого a и x ∈ ℝ мера $(-∞, x]$ по мере Стильтьджеса равна значению соответствующей функции Стильтьджеса: ENNReal.ofReal(stieltjesOfMeasurableRat f hf a x).

LaTeX

$$$(stieltjesOfMeasurableRat f hf a).\text{measure}((-\infty, x]) = \mathrm{ENNReal}.ofReal\left(stieltjesOfMeasurableRat f hf a x\right)$$$

Lean4

theorem measure_stieltjesOfMeasurableRat_Iic (hf : Measurable f) (a : α) (x : ℝ) :
    (stieltjesOfMeasurableRat f hf a).measure (Iic x) = ENNReal.ofReal (stieltjesOfMeasurableRat f hf a x) :=
  IsMeasurableRatCDF.measure_stieltjesFunction_Iic _ _ _

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