tendsto_coe_atTop — Mathlib

English

The map Real.toEReal: ℝ → EReal is continuous at the real at infinity point; it sends atTop to nhds top in EReal.

Русский

Отображение Real.toEReal: ℝ → EReal непрерывно в направлении бесконечности, и при пределе к +∞ оно стремится к верхней окрестности ⊤ в EReal.

LaTeX

$$$ \operatorname{Tendsto}(\mathrm{Real.toEReal})\, \mathrm{atTop}\, (\mathcal{N}_{\top}) $$$

Lean4

theorem tendsto_coe_atTop : Tendsto Real.toEReal atTop (𝓝 ⊤) :=
  tendsto_coe_nhds_top_iff.2 tendsto_id

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