tendsto_toReal — Mathlib

English

For a real-valued EReal element a with ⊤ and ⊥ excluded, the map toReal is a limit-preserving lift: Tendsto EReal.toReal (𝓝 a) (𝓝 a.toReal).

Русский

Для элемента EReal, исключающего бесконечности, отображение к действительным сохраняет пределы: Tendsto EReal.toReal (𝓝 a) (𝓝 a.toReal).

LaTeX

$$$\\text{tendsto } EReal.toReal\\ (\\mathcal{N}(a))\\ (\\mathcal{N}(a^{\\mathrm{toReal}}))$$$

Lean4

theorem tendsto_toReal {a : EReal} (ha : a ≠ ⊤) (h'a : a ≠ ⊥) : Tendsto EReal.toReal (𝓝 a) (𝓝 a.toReal) :=
  by
  lift a to ℝ using ⟨ha, h'a⟩
  rw [nhds_coe, tendsto_map'_iff]
  exact tendsto_id

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