tendsto_coe_toNNReal — Mathlib

English

For a ≠ ∞, the map ↑ from NNReal tends to ENNReal at a.fromNNReal, i.e., Tendsto (↑) (𝓝 a.toNNReal) (𝓝 a).

Русский

Для a ≠ ∞ переход через отображение ↑ к ENNReal сходится: Tendsto(↑) (𝓝 a.toNNReal) (𝓝 a).

LaTeX

$$$\\operatorname{Tendsto}(\\uparrow) (\\mathcal{N}(a^{\\mathrm{toNNReal}})) (\\mathcal{N}(a))$$$

Lean4

theorem tendsto_coe_toNNReal {a : ℝ≥0∞} (ha : a ≠ ⊤) : Tendsto (↑) (𝓝 a.toNNReal) (𝓝 a) :=
  by
  nth_rewrite 2 [← coe_toNNReal ha]
  exact continuous_coe.tendsto _

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