tendsto_ofReal_atTop_cobounded — Mathlib

English

The map ofReal from Real to 𝕜 is Tendsto from atTop to cobounded 𝕜, reflecting growth to infinity in the cobounded sense.

Русский

Отображение ofReal из Real в 𝕜 сходится от atTop к cobounded 𝕜, т.е. растет через границы cobounded.

LaTeX

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

Lean4

theorem tendsto_ofReal_atTop_cobounded : Tendsto ofReal atTop (Bornology.cobounded 𝕜) :=
  tendsto_norm_atTop_iff_cobounded.mp (mod_cast tendsto_abs_atTop_atTop)

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