tendsto_ofReal_atBot_cobounded — Mathlib

English

The map ofReal is Tendsto from atBot to cobounded 𝕜, capturing the behavior toward negative infinity in cobounded sense.

Русский

Отображение ofReal от atBot к cobounded 𝕜, описывающее поведение при стремлении к минус бесконечности.

LaTeX

$$$\mathrm{Tendsto} \mathrm{ofReal} (\mathrm{atBot}) (\text{cobounded } 𝕜)$$$

Lean4

theorem tendsto_ofReal_atBot_cobounded : Tendsto ofReal atBot (Bornology.cobounded 𝕜) :=
  tendsto_norm_atTop_iff_cobounded.mp (mod_cast tendsto_abs_atBot_atTop)

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