English
For any filter f, any function m: α → R and any a ∈ R, the convergence of m into the reals corresponds exactly to the convergence of its coe image into EReal: Tendsto (a ↦ m(a) : EReal) f (𝓝 ↑a) ⇔ Tendsto m f (𝓝 a).
Русский
Для любого фильтра f, функции m: α → R и числа a ∈ R выполнение перехода к a в реалах эквивалентно переходу к a в EReal через отображение включения: Tendsto (a ↦ m(a) : EReal) f (𝓝 ↑a) ⇔ Tendsto m f (𝓝 a).
LaTeX
$$$\\ Tendsto (\\\\lambda a. (m(a) : \\mathrm{EReal}))\; f\; (\\mathcal{N}\\, \\uparrow a) \\;\\Longleftrightarrow\\; Tendsto\; m\\ f\\ (\\mathcal{N}\\ a)$$$
Lean4
@[norm_cast]
theorem tendsto_coe {α : Type*} {f : Filter α} {m : α → ℝ} {a : ℝ} :
Tendsto (fun a => (m a : EReal)) f (𝓝 ↑a) ↔ Tendsto m f (𝓝 a) :=
isEmbedding_coe.tendsto_nhds_iff.symm
