stieltjesOfMeasurableRat_eq — Mathlib

English

For measurable f, and any a, r (rational), stieltjesOfMeasurableRat f hf a r equals toRatCDF f a r; in Loewner form, the toFun agrees at cast r.

Русский

Для измеримой f и любого a и рационального r выполняется равенство stieltjesOfMeasurableRat f hf a r = toRatCDF f a r; для коэффициента в cast соответствий совпадает.

LaTeX

$$$\forall a \in \alpha, \forall r \in \mathbb{Q},\; stieltjesOfMeasurableRat(f,hf,a)(r) = toRatCDF(f,a,r)$$$

Lean4

theorem stieltjesOfMeasurableRat_eq (hf : Measurable f) (a : α) (r : ℚ) :
    stieltjesOfMeasurableRat f hf a r = toRatCDF f a r :=
  IsMeasurableRatCDF.stieltjesFunction_eq _ a r

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