tendsto_cdf_atBot

Mathlib.Probability.CDF

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

English

As x tends to −∞, the cdf tends to 0.

Русский

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

LaTeX

$$$ \lim_{x \to -\infty} cdf(\mu)(x) = 0 $$$

Lean4

/-- The cdf tends to 0 at -∞. -/
theorem tendsto_cdf_atBot : Tendsto (cdf μ) atBot (𝓝 0) :=
  tendsto_condCDF_atBot _ _

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

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

Разделы

Аффилиация

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