tendsto_coe_nhds_bot_iff — Mathlib

English

For any f: α → Real, the convergence of the composed function x ↦ (f x).toEReal to nhdsBot is equivalent to f → atBot.

Русский

Для функции f: α → ℝ схождение x ↦ (f(x)).toEReal к nhdsBot эквивалентно тому, что f стремится к ⊥ по фильтру.

LaTeX

$$$ \operatorname{Tendsto}(\lambda x. (f(x)).\!\mathrm{toEReal})\, l\, (\mathcal{N}_{\bot}) \iff \operatorname{Tendsto} f\, l\ atBot $$$

Lean4

@[simp]
theorem tendsto_coe_nhds_bot_iff {f : α → ℝ} {l : Filter α} :
    Tendsto (fun x ↦ Real.toEReal (f x)) l (𝓝 ⊥) ↔ Tendsto f l atBot := by
  rw [tendsto_nhds_bot_iff_real, atBot_basis_Iio.tendsto_right_iff]; simp

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