measurable_toRatCDF

Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.measurable_toRatCDF

← MathLib Explorer

English

If f is measurable, then the regularized function toRatCDF f is measurable.

Русский

Если f измерима, то нормализованная функция toRatCDF f измерима.

LaTeX

$$$$\\text{Measurable}(\\mathrm{toRatCDF}(f)).$$$$

Lean4

theorem measurable_toRatCDF (hf : Measurable f) : Measurable (toRatCDF f) :=
  Measurable.ite (measurableSet_isRatStieltjesPoint hf) hf measurable_const

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru