isRatStieltjesPoint_defaultRatCDF

English

For every element a, the map q ↦ defaultRatCDF(q) has the Rat-Stieltjes property at a.

Русский

Для каждого элемента a отображение q ↦ defaultRatCDF(q) имеет свойство Rat-Stieltjes в точке a.

LaTeX

$$$$\\mathrm{IsRatStieltjesPoint}(\\lambda a. \\mathrm{defaultRatCDF})\,a,$$$$

Lean4

theorem isRatStieltjesPoint_defaultRatCDF (a : α) : IsRatStieltjesPoint (fun (_ : α) ↦ defaultRatCDF) a
    where
  mono := monotone_defaultRatCDF
  tendsto_atTop_one := tendsto_defaultRatCDF_atTop
  tendsto_atBot_zero := tendsto_defaultRatCDF_atBot
  iInf_rat_gt_eq := iInf_rat_gt_defaultRatCDF

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