tendsto_atBot_zero

Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.IsMeasurableRatCDF.tendsto_atBot_zero

← MathLib Explorer

English

As q goes to -∞, defaultRatCDF(q) tends to 0.

Русский

При стремлении q к -∞ функция defaultRatCDF(q) стремится к 0.

LaTeX

$$$\\mathrm{Tendsto}(\\mathrm{defaultRatCDF},\\mathrm{atBot},(\\mathcal{N}))$ к нулю$$

Lean4

theorem tendsto_atBot_zero {f : α → ℚ → ℝ} (hf : IsMeasurableRatCDF f) (a : α) : Tendsto (f a) atBot (𝓝 0) :=
  (hf.isRatStieltjesPoint a).tendsto_atBot_zero

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

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

Разделы

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

Аффилиация

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