measure_stieltjesOfMeasurableRat_univ

English

For every a, the univ-measure of the Stieltjes measure is 1, i.e., the total mass is 1.

Русский

Для каждого a сумма по всей множестве равна единице: μ_a(ℝ) = 1.

LaTeX

$$$(stieltjesOfMeasurableRat f hf a).\text{measure}(\mathbb{R}) = 1$$$

Lean4

theorem measure_stieltjesOfMeasurableRat_univ (hf : Measurable f) (a : α) :
    (stieltjesOfMeasurableRat f hf a).measure univ = 1 :=
  IsMeasurableRatCDF.measure_stieltjesFunction_univ _ _

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