isMeasurableRatCDF_toRatCDF — Mathlib

English

If f is measurable, then toRatCDF f is a measurable Rat-CDF object in the sense IsMeasurableRatCDF.

Русский

Если f измерима, то toRatCDF f является измеримой функцией-CDF по отношению к Раt.

LaTeX

$$$$\\mathrm{IsMeasurableRatCDF}(\\mathrm{toRatCDF}(f)).$$$$

Lean4

theorem isMeasurableRatCDF_toRatCDF (hf : Measurable f) : IsMeasurableRatCDF (toRatCDF f)
    where
  isRatStieltjesPoint
    a := by
    classical exact IsRatStieltjesPoint.ite (IsRatStieltjesPoint f) id (fun _ ↦ isRatStieltjesPoint_defaultRatCDF a)
  measurable := measurable_toRatCDF hf

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