toRatCDF_of_isRatStieltjesPoint — Mathlib

English

If a is a Rat-Stieltjes point for f, then for any rational q, toRatCDF f a q = f a q.

Русский

Если a является точкой Rat-Stieltjes для f, то для всякого рационального q выполняется toRatCDF f a q = f a q.

LaTeX

$$$$\\text{toRatCDF}(f)(a)(q) = f(a,q) \\quad \\text{whenever } \\mathrm{IsRatStieltjesPoint}(f,a).$$$$

Lean4

theorem toRatCDF_of_isRatStieltjesPoint {a : α} (h : IsRatStieltjesPoint f a) (q : ℚ) : toRatCDF f a q = f a q := by
  rw [toRatCDF, if_pos h]

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