tendsto_coe_nhds_top_iff — Mathlib

English

For any function f: α → ℝ, the statement that the composed function x ↦ Real.toEReal(f x) tends to ⊤ under l is equivalent to f tending to +∞ along l.

Русский

Для функции f: α → ℝ равносильна, что отображение x ↦ Real.toEReal(f(x)) стремится к верхнему пределу ⊤ по фильтру l, и что f стремится к +∞ по l.

LaTeX

$$$ \operatorname{Tendsto}(\lambda x. \mathrm{Real.toEReal}(f(x)))\, l\, 𝓝(\top) \;\iff\; \operatorname{Tendsto} f\, l\ \text{atTop} $$$

Lean4

@[simp]
theorem tendsto_coe_nhds_top_iff {f : α → ℝ} {l : Filter α} :
    Tendsto (fun x ↦ Real.toEReal (f x)) l (𝓝 ⊤) ↔ Tendsto f l atTop := by
  rw [tendsto_nhds_top_iff_real, atTop_basis_Ioi.tendsto_right_iff]; simp

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