tendsto_atTop_one

Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

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

← MathLib Explorer

English

As q grows to +∞, defaultRatCDF(q) tends to 1.

Русский

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

LaTeX

$$$\\mathrm{Tendsto}(\\mathrm{defaultRatCDF},\\mathrm{atTop},(\\mathcal{N} variables))$ в смысле к единице$$

Lean4

theorem tendsto_atTop_one {f : α → ℚ → ℝ} (hf : IsMeasurableRatCDF f) (a : α) : Tendsto (f a) atTop (𝓝 1) :=
  (hf.isRatStieltjesPoint a).tendsto_atTop_one

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

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

Разделы

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

Аффилиация

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