tendsto_toReal_atTop — Mathlib

English

As one approaches the top from below, the real-valued toReal map tends to +∞ along the atTop direction.

Русский

При подходе к ⊤ снизу функция toReal сходится к +∞ вдоль направления atTop.

LaTeX

$$$ \operatorname{Tendsto}(\mathrm{EReal.toReal})\, (\mathcal{N}_{\neq} \top)\, atTop $$$

Lean4

theorem tendsto_toReal_atTop : Tendsto EReal.toReal (𝓝[≠] ⊤) atTop :=
  by
  rw [nhdsWithin_top, tendsto_map'_iff]
  exact tendsto_id

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