tendsto_toReal

Mathlib.Topology.Instances.ENNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#ENNReal.tendsto_toReal

English

For a ≠ ∞, Tendsto ENNReal.toReal (nhds a) (nhds a.toReal) holds.

Русский

Для a ≠ ∞ имеет место Tendsto ENNReal.toReal (nhds a) (nhds a.toReal).

LaTeX

$$$\\operatorname{Tendsto} \\mathrm{ENNReal}.toReal (\\mathcal{N}(a)) (\\mathcal{N}(a^{\\mathrm{toReal}}))$$$

Lean4

theorem tendsto_toReal {a : ℝ≥0∞} (ha : a ≠ ∞) : Tendsto ENNReal.toReal (𝓝 a) (𝓝 a.toReal) :=
  NNReal.tendsto_coe.2 <| tendsto_toNNReal ha

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru