tendsto_inv_iff₀ — Mathlib

English

If x ≠ 0, then the convergence of the inverse sequence f(x)⁻¹ to x⁻¹ is equivalent to the convergence of f(x) to x.

Русский

Если x ≠ 0, то сходимость обратного образа f(x)⁻¹ к x⁻¹ эквивалентна сходимости f(x) к x.

LaTeX

$$x \\neq 0 \\Rightarrow \\operatorname{Tendsto} (\\lambda x, f(x)^{-1}) l (\\mathcal{N}(x^{-1})) \\iff \\operatorname{Tendsto} f l (\\mathcal{N}(x))$$

Lean4

theorem tendsto_inv_iff₀ {l : Filter α} {f : α → G₀} (hx : x ≠ 0) :
    Tendsto (fun x ↦ (f x)⁻¹) l (𝓝 x⁻¹) ↔ Tendsto f l (𝓝 x) := by
  simp only [nhds_inv₀ hx, ← Filter.comap_inv, tendsto_comap_iff, Function.comp_def, inv_inv]

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