tendsto_cdf_atTop

Mathlib.Probability.CDF

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

English

As x tends to +∞, the cdf tends to 1.

Русский

Пусть x стремится к +∞; предел Fμ(x) равен 1.

LaTeX

$$$ \lim_{x \to +\infty} cdf(\mu)(x) = 1 $$$

Lean4

/-- The cdf tends to 1 at +∞. -/
theorem tendsto_cdf_atTop : Tendsto (cdf μ) atTop (𝓝 1) :=
  tendsto_condCDF_atTop _ _

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

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

Разделы

Аффилиация

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